1  /-
  2  Copyright (c) 2017 Microsoft Corporation. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Leonardo de Moura
  5  -/
  6  import data.rbtree.find
src         └──────────────┘
  7  universes u v
  8  
  9  local attribute [simp] rbnode.lift
id                          └─────────┘
src                         └─────────┘
typ                         └─────────┘
doc                   └──┘
 10  
 11  namespace rbnode
 12  variables {α : Type u}
 13  
 14  open color
 15  
 16  @[simp] lemma balance1_eq₁ (l : rbnode α) (x r₁ y r₂ v t) : balance1 (red_node l x r₁) y r₂ v t = red_node (black_node l x r₁) y (black_node r₂ v t) :=
id                                   └────┘                     └──────┘  └──────┘   └┘   └┘    └──────┘  └────────┘   └┘    └────────┘ └┘  
src                                  └────┘                      └──────┘  └──────┘                   └──────┘  └────────┘            └────────┘
typ                                  └────┘                     └──────┘  └──────┘   └┘   └┘    └──────┘  └────────┘   └┘    └────────┘ └┘  
doc    └──┘
 17  begin cases r₂; refl end
id               └┘
src        └────┘    └───┘
typ        └────┘└┘  └───┘
doc        └────┘    └───┘
txt        └────┘    └───┘
par        └────┘    └───┘
pid                     
st   └───────────────────┘└─┘
 18  
 19  @[simp] lemma balance1_eq₂ (l₁ : rbnode α) (y l₂ x r v t) : get_color l₁ ≠ red → balance1 l₁ y (red_node l₂ x r)  v t = red_node (black_node l₁ y l₂) x (black_node r v t) :=
id                                    └────┘                    └───────┘ └┘  └─┘   └──────┘ └┘   └──────┘ └┘        └──────┘  └────────┘ └┘  └┘    └────────┘   
src                                   └────┘                     └───────┘     └─┘   └──────┘       └──────┘               └──────┘  └────────┘             └────────┘
typ                                   └────┘                    └───────┘ └┘  └─┘   └──────┘ └┘   └──────┘ └┘        └──────┘  └────────┘ └┘  └┘    └────────┘   
doc    └──┘
 20  begin cases l₁; simp [get_color, balance1] end
id               └┘        └───────┘  └──────┘
src        └────┘    └────┘└───────┘└┘└──────┘└┘
typ        └────┘└┘  └────┘└───────┘└┘└──────┘└┘
doc        └────┘    └────┘         └┘        └┘
txt        └────┘    └────┘         └┘        └┘
par        └────┘    └────┘         └┘        └┘
pid                              └┘        
st   └─────────────────────────────────────────┘└─┘
 21  
 22  @[simp] lemma balance1_eq₃ (l : rbnode α) (y r v t) : get_color l ≠ red → get_color r ≠ red → balance1 l y r v t = black_node (red_node l y r) v t :=
id                                   └────┘               └───────┘   └─┘   └───────┘   └─┘   └──────┘       └────────┘  └──────┘      
src                                  └────┘                └───────┘    └─┘   └───────┘    └─┘   └──────┘            └────────┘  └──────┘
typ                                  └────┘               └───────┘   └─┘   └───────┘   └─┘   └──────┘       └────────┘  └──────┘      
doc    └──┘
 23  begin cases l; cases r; simp [get_color, balance1] end
id                               └───────┘  └──────┘
src        └────┘   └────┘   └────┘└───────┘└┘└──────┘└┘
typ        └────┘  └────┘  └────┘└───────┘└┘└──────┘└┘
doc        └────┘   └────┘   └────┘         └┘        └┘
txt        └────┘   └────┘   └────┘         └┘        └┘
par        └────┘   └────┘   └────┘         └┘        └┘
pid                                     └┘        
st   └─────────────────────────────────────────────────┘└─┘
 24  
 25  @[simp] lemma balance2_eq₁ (l : rbnode α) (x₁ r₁ y r₂ v t) : balance2 (red_node l x₁ r₁) y r₂  v t = red_node (black_node t v l) x₁ (black_node r₁ y r₂) :=
id                                   └────┘                      └──────┘  └──────┘  └┘ └┘   └┘     └──────┘  └────────┘     └┘  └────────┘ └┘  └┘
src                                  └────┘                       └──────┘  └──────┘                     └──────┘  └────────┘            └────────┘
typ                                  └────┘                      └──────┘  └──────┘  └┘ └┘   └┘     └──────┘  └────────┘     └┘  └────────┘ └┘  └┘
doc    └──┘
 26  by cases r₂; refl
id            └┘
src     └────┘    └────
typ     └────┘└┘  └────
doc     └────┘    └────
txt     └────┘    └────
par     └────┘    └────
pid                  
st     └───────────────
 27  
src  
typ  
doc  
txt  
par  
pid  
st   
 28  @[simp] lemma balance2_eq₂ (l₁ : rbnode α) (y l₂ x₂ r₂ v t) : get_color l₁ ≠ red → balance2 l₁ y (red_node l₂ x₂ r₂) v t = red_node (black_node t v l₁) y (black_node l₂ x₂ r₂) :=
id                                    └────┘                      └───────┘ └┘  └─┘   └──────┘ └┘   └──────┘ └┘ └┘ └┘     └──────┘  └────────┘   └┘    └────────┘ └┘ └┘ └┘
src                                   └────┘                       └───────┘     └─┘   └──────┘       └──────┘                └──────┘  └────────┘            └────────┘
typ                                   └────┘                      └───────┘ └┘  └─┘   └──────┘ └┘   └──────┘ └┘ └┘ └┘     └──────┘  └────────┘   └┘    └────────┘ └┘ └┘ └┘
doc    └──┘
 29  begin cases l₁; simp [get_color, balance2] end
id               └┘        └───────┘  └──────┘
src        └────┘    └────┘└───────┘└┘└──────┘└┘
typ        └────┘└┘  └────┘└───────┘└┘└──────┘└┘
doc        └────┘    └────┘         └┘        └┘
txt        └────┘    └────┘         └┘        └┘
par        └────┘    └────┘         └┘        └┘
pid                              └┘        
st   └─────────────────────────────────────────┘└─┘
 30  
 31  @[simp] lemma balance2_eq₃ (l : rbnode α) (y r v t) : get_color l ≠ red → get_color r ≠ red → balance2 l  y r  v t = black_node t v (red_node l y r) :=
id                                   └────┘               └───────┘   └─┘   └───────┘   └─┘   └──────┘         └────────┘    └──────┘   
src                                  └────┘                └───────┘    └─┘   └───────┘    └─┘   └──────┘              └────────┘      └──────┘
typ                                  └────┘               └───────┘   └─┘   └───────┘   └─┘   └──────┘         └────────┘    └──────┘   
doc    └──┘
 32  begin cases l; cases r; simp [get_color, balance2] end
id                               └───────┘  └──────┘
src        └────┘   └────┘   └────┘└───────┘└┘└──────┘└┘
typ        └────┘  └────┘  └────┘└───────┘└┘└──────┘└┘
doc        └────┘   └────┘   └────┘         └┘        └┘
txt        └────┘   └────┘   └────┘         └┘        └┘
par        └────┘   └────┘   └────┘         └┘        └┘
pid                                     └┘        
st   └─────────────────────────────────────────────────┘└─┘
 33  
 34  /- We can use the same induction principle for balance1 and balance2 -/
 35  lemma balance.cases {p : rbnode α → α → rbnode α → Prop}
id                            └────┘       └────┘ 
src                           └────┘         └────┘
typ                           └────┘       └────┘ 
 36    (l y r)
 37    (red_left : ∀ l x r₁ y r₂, p (red_node l x r₁) y r₂)
id                     └┘  └┘    └──────┘   └┘   └┘
src                                  └──────┘
typ                    └┘  └┘    └──────┘   └┘   └┘
 38    (red_right : ∀ l₁ y l₂ x r, get_color l₁ ≠ red → p l₁ y (red_node l₂ x r))
id                    └┘  └┘    └───────┘ └┘  └─┘    └┘   └──────┘ └┘  
src                                └───────┘     └─┘           └──────┘
typ                   └┘  └┘    └───────┘ └┘  └─┘    └┘   └──────┘ └┘  
 39    (other : ∀ l y r, get_color l ≠ red → get_color r ≠ red → p l y r)
id                    └───────┘   └─┘   └───────┘   └─┘      
src                      └───────┘    └─┘   └───────┘    └─┘
typ                   └───────┘   └─┘   └───────┘   └─┘      
st                      └───────┘
 40    : p l y r :=
id          
typ         
 41  begin
st   └─────
 42    cases l; cases r,
id                   
src    └────┘   └────┘
typ    └────┘  └────┘
doc    └────┘   └────┘
txt    └────┘   └────┘
par    └────┘   └────┘
pid                 
st   ─────────────────┘└─
 43    any_goals { apply red_left },
src    └──────────┘└────┘        
typ    └──────────┘└────┘        
doc    └──────────┘└────┘        
txt    └──────────┘└────┘        
par    └──────────┘└────┘        
pid             └───────┘        └┘
st   ────────────┘└──────────────┘└┘
 44    any_goals { apply red_right; simp [get_color]; contradiction; done },
id                                        └───────┘
src    └──────────┘└────┘         └┘└────┘└───────┘└┘└───────────┘└┘└───┘
typ    └──────────┘└────┘         └┘└────┘└───────┘└┘└───────────┘└┘└───┘
doc    └──────────┘└────┘         └┘└────┘         └┘└───────────┘└┘└───┘
txt    └──────────┘└────┘         └┘└────┘         └┘└───────────┘└┘└───┘
par    └──────────┘└────┘         └┘└────┘         └┘└───────────┘└┘└───┘
pid             └───────┘         └──────┘         └──────────────────────┘
st   ────────────┘└──────────────────────────────────────────────────────┘└┘
 45    any_goals { apply other; simp [get_color]; contradiction; done },
id                                    └───────┘
src    └──────────┘└────┘     └┘└────┘└───────┘└┘└───────────┘└┘└───┘
typ    └──────────┘└────┘     └┘└────┘└───────┘└┘└───────────┘└┘└───┘
doc    └──────────┘└────┘     └┘└────┘         └┘└───────────┘└┘└───┘
txt    └──────────┘└────┘     └┘└────┘         └┘└───────────┘└┘└───┘
par    └──────────┘└────┘     └┘└────┘         └┘└───────────┘└┘└───┘
pid             └───────┘     └──────┘         └──────────────────────┘
st   ────────────┘└──────────────────────────────────────────────────┘└──
 46  end
st   ──┘
 47  
 48  lemma balance1_ne_leaf (l : rbnode α) (x r v t) : balance1 l x r v t ≠ leaf :=
id                               └────┘               └──────┘       └──┘
src                              └────┘                └──────┘            └──┘
typ                              └────┘               └──────┘       └──┘
 49  by apply balance.cases l x r; intros; simp [*]; contradiction
id            └───────────┘   
src     └────┘└───────────┘     └────┘  └──────┘  └─────────────
typ     └────┘└───────────┘  └────┘  └──────┘  └─────────────
doc     └────┘                  └────┘  └──────┘  └─────────────
txt     └────┘                  └────┘  └──────┘  └─────────────
par     └────┘                  └────┘  └──────┘  └─────────────
pid                                        └─┘               
st     └───────────────────────────────────────────────────────────
 50  
src  
typ  
doc  
txt  
par  
pid  
st   
 51  lemma balance1_node_ne_leaf {s : rbnode α} (a : α) (t : rbnode α) : s ≠ leaf → balance1_node s a t ≠ leaf :=
id                                    └────┘               └────┘       └──┘   └───────────┘     └──┘
src                                   └────┘                 └────┘         └──┘   └───────────┘        └──┘
typ                                   └────┘               └────┘       └──┘   └───────────┘     └──┘
 52  begin
st   └─────
 53    intro h, cases s,
id                    
src    └─────┘  └────┘
typ    └─────┘  └────┘
doc    └─────┘  └────┘
txt    └─────┘  └────┘
par    └─────┘  └────┘
pid         └┘       
st   ────────┘└───────┘└─
 54    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
 55    all_goals { simp [balance1_node], apply balance1_ne_leaf }
id                       └───────────┘         └──────────────┘
src    └──────────┘└────┘└───────────┘└┘└────┘└──────────────┘└┘
typ    └──────────┘└────┘└───────────┘└┘└────┘└──────────────┘└┘
doc    └──────────┘└────┘             └┘└────┘                └┘
txt    └──────────┘└────┘             └┘└────┘                └┘
par    └──────────┘└────┘             └┘└────┘                └┘
pid             └───────┘             └───────┘                └┘
st   ────────────┘└───────────────────┘└───────────────────────┘
 56  end
st   └─┘
 57  
 58  lemma balance2_ne_leaf (l : rbnode α) (x r v t) : balance2 l x r v t ≠ leaf :=
id                               └────┘               └──────┘       └──┘
src                              └────┘                └──────┘            └──┘
typ                              └────┘               └──────┘       └──┘
 59  by apply balance.cases l x r; intros; simp [*]; contradiction
id            └───────────┘   
src     └────┘└───────────┘     └────┘  └──────┘  └─────────────
typ     └────┘└───────────┘  └────┘  └──────┘  └─────────────
doc     └────┘                  └────┘  └──────┘  └─────────────
txt     └────┘                  └────┘  └──────┘  └─────────────
par     └────┘                  └────┘  └──────┘  └─────────────
pid                                        └─┘               
st     └───────────────────────────────────────────────────────────
 60  
src  
typ  
doc  
txt  
par  
pid  
st   
 61  lemma balance2_node_ne_leaf {s : rbnode α} (a : α) (t : rbnode α) : s ≠ leaf → balance2_node s a t ≠ leaf :=
id                                    └────┘               └────┘       └──┘   └───────────┘     └──┘
src                                   └────┘                 └────┘         └──┘   └───────────┘        └──┘
typ                                   └────┘               └────┘       └──┘   └───────────┘     └──┘
 62  begin
st   └─────
 63    intro h, cases s,
id                    
src    └─────┘  └────┘
typ    └─────┘  └────┘
doc    └─────┘  └────┘
txt    └─────┘  └────┘
par    └─────┘  └────┘
pid         └┘       
st   ────────┘└───────┘└─
 64    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
 65    all_goals { simp [balance2_node], apply balance2_ne_leaf }
id                       └───────────┘         └──────────────┘
src    └──────────┘└────┘└───────────┘└┘└────┘└──────────────┘└┘
typ    └──────────┘└────┘└───────────┘└┘└────┘└──────────────┘└┘
doc    └──────────┘└────┘             └┘└────┘                └┘
txt    └──────────┘└────┘             └┘└────┘                └┘
par    └──────────┘└────┘             └┘└────┘                └┘
pid             └───────┘             └───────┘                └┘
st   ────────────┘└───────────────────┘└───────────────────────┘
 66  end
st   └─┘
 67  
 68  variables (lt : α → α → Prop) [decidable_rel lt]
id                                  └───────────┘
src                                 └───────────┘
typ                                 └───────────┘
 69  
 70  @[elab_as_eliminator]
doc    └────────────────┘
 71  lemma ins.induction {p : rbnode α → Prop}
id                            └────┘ 
src                           └────┘
typ                           └────┘ 
 72    (t x)
 73    (is_leaf : p leaf)
id                 └──┘
src                 └──┘
typ                └──┘
 74    (is_red_lt : ∀ a y b (hc : cmp_using lt x y = ordering.lt) (ih : p a), p (red_node a y b))
id                             └───────┘ └┘    └─────────┘              └──────┘   
src                               └───────┘         └─────────┘                 └──────┘
typ                            └───────┘ └┘    └─────────┘              └──────┘   
 75    (is_red_eq : ∀ a y b (hc : cmp_using lt x y = ordering.eq), p (red_node a y b))
id                             └───────┘ └┘    └─────────┘     └──────┘   
src                               └───────┘         └─────────┘      └──────┘
typ                            └───────┘ └┘    └─────────┘     └──────┘   
 76    (is_red_gt : ∀ a y b (hc : cmp_using lt x y = ordering.gt) (ih : p b), p (red_node a y b))
id                             └───────┘ └┘    └─────────┘              └──────┘   
src                               └───────┘         └─────────┘                 └──────┘
typ                            └───────┘ └┘    └─────────┘              └──────┘   
 77    (is_black_lt_red : ∀ a y b (hc : cmp_using lt x y = ordering.lt) (hr : get_color a = red) (ih : p a), p (black_node a y b))
id                                   └───────┘ └┘    └─────────┘        └───────┘   └─┘              └────────┘   
src                                     └───────┘         └─────────┘        └───────┘    └─┘                 └────────┘
typ                                  └───────┘ └┘    └─────────┘        └───────┘   └─┘              └────────┘   
 78    (is_black_lt_not_red : ∀ a y b (hc : cmp_using lt x y = ordering.lt) (hnr : get_color a ≠ red) (ih : p a), p (black_node a y b))
id                                       └───────┘ └┘    └─────────┘         └───────┘   └─┘              └────────┘   
src                                         └───────┘         └─────────┘         └───────┘    └─┘                 └────────┘
typ                                      └───────┘ └┘    └─────────┘         └───────┘   └─┘              └────────┘   
 79    (is_black_eq : ∀ a y b (hc : cmp_using lt x y = ordering.eq), p (black_node a y b))
id                               └───────┘ └┘    └─────────┘     └────────┘   
src                                 └───────┘         └─────────┘      └────────┘
typ                              └───────┘ └┘    └─────────┘     └────────┘   
 80    (is_black_gt_red : ∀ a y b (hc : cmp_using lt x y = ordering.gt) (hr : get_color b = red) (ih : p b), p (black_node a y b))
id                                   └───────┘ └┘    └─────────┘        └───────┘   └─┘              └────────┘   
src                                     └───────┘         └─────────┘        └───────┘    └─┘                 └────────┘
typ                                  └───────┘ └┘    └─────────┘        └───────┘   └─┘              └────────┘   
 81    (is_black_gt_not_red : ∀ a y b (hc : cmp_using lt x y = ordering.gt) (hnr : get_color b ≠ red) (ih : p b), p (black_node a y b))
id                                       └───────┘ └┘    └─────────┘         └───────┘   └─┘              └────────┘   
src                                         └───────┘         └─────────┘         └───────┘    └─┘                 └────────┘
typ                                      └───────┘ └┘    └─────────┘         └───────┘   └─┘              └────────┘   
 82    : p t :=
id        
typ       
 83  begin
st   └─────
 84    induction t,
id               
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ────────────┘└─
 85    case leaf { apply is_leaf },
src    └──────────┘└────┘       
typ    └──────────┘└────┘       
doc    └──────────┘└────┘       
txt    └──────────┘└────┘       
par    └──────────┘└────┘       
pid        └───┘└──────┘       └┘
st   ────────────┘└─────────────┘└┘
 86    case red_node : a y b {
src    └───────────────────────
typ    └───────────────────────
doc    └───────────────────────
txt    └───────────────────────
par    └───────────────────────
pid        └───────┘└──────┘└──
st   ────────────────────────┘
 87       cases h : cmp_using lt x y,
id                  └───────┘ └┘  
src  ────┘└────┘ └─┘└───────┘    └─
typ  ────┘└────┘ └─┘└───────┘└┘└─
doc  ────┘└────┘ └─┘             └─
txt  ────┘└────┘ └─┘             └─
par  ────┘└────┘ └─┘             └─
pid  ──────────┘ └─┘             └─
st   ──────────────────────────────┘└─
 88       case ordering.lt { apply is_red_lt; assumption },
src  ───────────────────────┘└────┘         └┘└─────────┘└──
typ  ───────────────────────┘└────┘         └┘└─────────┘└──
doc  ───────────────────────┘└────┘         └┘└─────────┘└──
txt  ───────────────────────┘└────┘         └┘└─────────┘└──
par  ───────────────────────┘└────┘         └┘└─────────┘└──
pid  ─────────────────────────────┘         └───────────────
st   ──────────────────────┘└───────────────────────────┘└─
 89       case ordering.eq { apply is_red_eq; assumption },
src  ───────────────────────┘└────┘         └┘└─────────┘└──
typ  ───────────────────────┘└────┘         └┘└─────────┘└──
doc  ───────────────────────┘└────┘         └┘└─────────┘└──
txt  ───────────────────────┘└────┘         └┘└─────────┘└──
par  ───────────────────────┘└────┘         └┘└─────────┘└──
pid  ─────────────────────────────┘         └───────────────
st   ──────────────────────┘└───────────────────────────┘└─
 90       case ordering.gt { apply is_red_gt; assumption },
src  ───────────────────────┘└────┘         └┘└─────────┘└──
typ  ───────────────────────┘└────┘         └┘└─────────┘└──
doc  ───────────────────────┘└────┘         └┘└─────────┘└──
txt  ───────────────────────┘└────┘         └┘└─────────┘└──
par  ───────────────────────┘└────┘         └┘└─────────┘└──
pid  ─────────────────────────────┘         └───────────────
st   ───────────────────────────────────────────────────┘└──
 91     },
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ────┘
 92    case black_node : a y b {
src    └─────────────────────────
typ    └─────────────────────────
doc    └─────────────────────────
txt    └─────────────────────────
par    └─────────────────────────
pid        └─────────┘└──────┘└──
st   ──────────────────────────┘
 93       cases h : cmp_using lt x y,
id                  └───────┘ └┘  
src  ────┘└────┘ └─┘└───────┘    └─
typ  ────┘└────┘ └─┘└───────┘└┘└─
doc  ────┘└────┘ └─┘             └─
txt  ────┘└────┘ └─┘             └─
par  ────┘└────┘ └─┘             └─
pid  ──────────┘ └─┘             └─
st   ──────────────────────────────┘└─
 94       case ordering.lt {
src  ────────────────────────
typ  ────────────────────────
doc  ────────────────────────
txt  ────────────────────────
par  ────────────────────────
pid  ────────────────────────
st   ──────────────────────┘
 95         by_cases get_color a = red,
id                   └───────┘    └─┘
src  ──────┘└───────┘└───────┘  └─┘└─
typ  ──────┘└───────┘└───────┘ └─┘└─
doc  ──────┘└───────┘              └─
txt  ──────┘└───────┘              └─
par  ──────┘└───────┘              └─
pid  ───────────────┘              └─
st   ────────────────────────────────┘└─
 96         { apply is_black_lt_red; assumption },
src  ────────┘└────┘               └┘└─────────┘└──
typ  ────────┘└────┘               └┘└─────────┘└──
doc  ────────┘└────┘               └┘└─────────┘└──
txt  ────────┘└────┘               └┘└─────────┘└──
par  ────────┘└────┘               └┘└─────────┘└──
pid  ──────────────┘               └───────────────
st   ───────┘└─────────────────────────────────┘└─
 97         { apply is_black_lt_not_red; assumption },
src  ────────┘└────┘                   └┘└─────────┘└──
typ  ────────┘└────┘                   └┘└─────────┘└──
doc  ────────┘└────┘                   └┘└─────────┘└──
txt  ────────┘└────┘                   └┘└─────────┘└──
par  ────────┘└────┘                   └┘└─────────┘└──
pid  ──────────────┘                   └───────────────
st   ──────────────────────────────────────────────┘└──
 98       },
src  ────────
typ  ────────
doc  ────────
txt  ────────
par  ────────
pid  ────────
st   ─────┘└─
 99       case ordering.eq { apply is_black_eq; assumption },
src  ───────────────────────┘└────┘           └┘└─────────┘└──
typ  ───────────────────────┘└────┘           └┘└─────────┘└──
doc  ───────────────────────┘└────┘           └┘└─────────┘└──
txt  ───────────────────────┘└────┘           └┘└─────────┘└──
par  ───────────────────────┘└────┘           └┘└─────────┘└──
pid  ─────────────────────────────┘           └───────────────
st   ──────────────────────┘└─────────────────────────────┘└─
100       case ordering.gt {
src  ────────────────────────
typ  ────────────────────────
doc  ────────────────────────
txt  ────────────────────────
par  ────────────────────────
pid  ────────────────────────
st   ────────────────────────
101         by_cases get_color b = red,
id                   └───────┘    └─┘
src  ──────┘└───────┘└───────┘  └─┘└─
typ  ──────┘└───────┘└───────┘ └─┘└─
doc  ──────┘└───────┘              └─
txt  ──────┘└───────┘              └─
par  ──────┘└───────┘              └─
pid  ───────────────┘              └─
st   ────────────────────────────────┘└─
102         { apply is_black_gt_red; assumption },
src  ────────┘└────┘               └┘└─────────┘└──
typ  ────────┘└────┘               └┘└─────────┘└──
doc  ────────┘└────┘               └┘└─────────┘└──
txt  ────────┘└────┘               └┘└─────────┘└──
par  ────────┘└────┘               └┘└─────────┘└──
pid  ──────────────┘               └───────────────
st   ───────┘└─────────────────────────────────┘└─
103         { apply is_black_gt_not_red; assumption },
src  ────────┘└────┘                   └┘└─────────┘└──
typ  ────────┘└────┘                   └┘└─────────┘└──
doc  ────────┘└────┘                   └┘└─────────┘└──
txt  ────────┘└────┘                   └┘└─────────┘└──
par  ────────┘└────┘                   └┘└─────────┘└──
pid  ──────────────┘                   └───────────────
st   ──────────────────────────────────────────────┘└──
104       }
src  ───────
typ  ───────
doc  ───────
txt  ───────
par  ───────
pid  ───────
st   ─────┘
105    }
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ──┘
st   ─┘
106  end
st   └─┘
107  
108  lemma is_searchable_balance1 {l y r v t lo hi} : is_searchable lt l lo (some y) →  is_searchable lt r (some y) (some v) → is_searchable lt t (some v) hi → is_searchable lt (balance1 l y r v t) lo hi :=
id                                                    └───────────┘ └┘  └┘  └──┘      └───────────┘ └┘   └──┘    └──┘     └───────────┘ └┘   └──┘   └┘   └───────────┘ └┘  └──────┘       └┘ └┘
src                                                   └───────────┘          └──┘       └───────────┘       └──┘     └──┘      └───────────┘       └──┘         └───────────┘     └──────┘
typ                                                   └───────────┘ └┘  └┘  └──┘      └───────────┘ └┘   └──┘    └──┘     └───────────┘ └┘   └──┘   └┘   └───────────┘ └┘  └──────┘       └┘ └┘
109  by apply balance.cases l y r; intros; simp [*]; is_searchable_tactic
id            └───────────┘                       └──────────────────┘
src     └────┘└───────────┘     └────┘  └──────┘  └──────────────────┘
typ     └────┘└───────────┘  └────┘  └──────┘  └──────────────────┘
doc     └────┘                  └────┘  └──────┘
txt     └────┘                  └────┘  └──────┘
par     └────┘                  └────┘  └──────┘  └──────────────────┘
pid                                        └─┘
st     └────────────────────────────────────────────────────────────────┘
110  
111  lemma is_searchable_balance1_node {t} [is_trans α lt] : ∀ {y s lo hi}, is_searchable lt t lo (some y) → is_searchable lt s (some y) hi → is_searchable lt (balance1_node t y s) lo hi :=
id                                          └──────┘  └┘         └┘ └┘   └───────────┘ └┘  └┘  └──┘     └───────────┘ └┘   └──┘   └┘   └───────────┘ └┘  └───────────┘     └┘ └┘
src                                         └──────┘                        └───────────┘          └──┘      └───────────┘       └──┘         └───────────┘     └───────────┘
typ                                         └──────┘  └┘         └┘ └┘   └───────────┘ └┘  └┘  └──┘     └───────────┘ └┘   └──┘   └┘   └───────────┘ └┘  └───────────┘     └┘ └┘
112  begin
st   └─────
113    cases t; simp!; intros; is_searchable_tactic,
id                            └──────────────────┘
src    └────┘   └───┘  └────┘  └──────────────────┘
typ    └────┘  └───┘  └────┘  └──────────────────┘
doc    └────┘   └───┘  └────┘
txt    └────┘   └───┘  └────┘
par    └────┘   └───┘  └────┘  └──────────────────┘
pid                
st   ─────────────────────────────────────────────┘└─
114    { cases lo,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└──────┘└─
115      { apply is_searchable_none_low_of_is_searchable_some_low, assumption },
id               └──────────────────────────────────────────────┘
src        └────┘└──────────────────────────────────────────────┘  └─────────┘
typ        └────┘└──────────────────────────────────────────────┘  └─────────┘
doc        └────┘                                                  └─────────┘
txt        └────┘                                                  └─────────┘
par        └────┘                                                  └─────────┘
pid                                                                         
st   ─────┘└────────────────────────────────────────────────────┘└───────────┘└┘
116      { simp at *, apply is_searchable_some_low_of_is_searchable_of_lt; assumption } },
id                          └───────────────────────────────────────────┘
src        └───────┘  └────┘└───────────────────────────────────────────┘  └─────────┘
typ        └───────┘  └────┘└───────────────────────────────────────────┘  └─────────┘
doc        └───────┘  └────┘                                               └─────────┘
txt        └───────┘  └────┘                                               └─────────┘
par        └───────┘  └────┘                                               └─────────┘
pid            └──┘                                                                
st   ──────────────┘└────────────────────────────────────────────────────────────────┘└──┘
117    all_goals { apply is_searchable_balance1; assumption }
id                       └────────────────────┘
src    └──────────┘└────┘└────────────────────┘└┘└─────────┘└┘
typ    └──────────┘└────┘└────────────────────┘└┘└─────────┘└┘
doc    └──────────┘└────┘                      └┘└─────────┘└┘
txt    └──────────┘└────┘                      └┘└─────────┘└┘
par    └──────────┘└────┘                      └┘└─────────┘└┘
pid             └───────┘                      └────────────┘
st   ────────────┘└────────────────────────────────────────┘
118  end
st   └─┘
119  
120  lemma is_searchable_balance2 {l y r v t lo hi} : is_searchable lt t lo (some v) → is_searchable lt l (some v) (some y) → is_searchable lt r (some y) hi → is_searchable lt (balance2 l y r v t) lo hi :=
id                                                    └───────────┘ └┘  └┘  └──┘     └───────────┘ └┘   └──┘    └──┘     └───────────┘ └┘   └──┘   └┘   └───────────┘ └┘  └──────┘       └┘ └┘
src                                                   └───────────┘          └──┘      └───────────┘       └──┘     └──┘      └───────────┘       └──┘         └───────────┘     └──────┘
typ                                                   └───────────┘ └┘  └┘  └──┘     └───────────┘ └┘   └──┘    └──┘     └───────────┘ └┘   └──┘   └┘   └───────────┘ └┘  └──────┘       └┘ └┘
121  by apply balance.cases l y r; intros; simp [*]; is_searchable_tactic
id            └───────────┘                       └──────────────────┘
src     └────┘└───────────┘     └────┘  └──────┘  └──────────────────┘
typ     └────┘└───────────┘  └────┘  └──────┘  └──────────────────┘
doc     └────┘                  └────┘  └──────┘
txt     └────┘                  └────┘  └──────┘
par     └────┘                  └────┘  └──────┘  └──────────────────┘
pid                                        └─┘
st     └────────────────────────────────────────────────────────────────┘
122  
123  lemma is_searchable_balance2_node {t} [is_trans α lt] : ∀ {y s lo hi}, is_searchable lt s lo (some y) → is_searchable lt t (some y) hi → is_searchable lt (balance2_node t y s) lo hi :=
id                                          └──────┘  └┘         └┘ └┘   └───────────┘ └┘  └┘  └──┘     └───────────┘ └┘   └──┘   └┘   └───────────┘ └┘  └───────────┘     └┘ └┘
src                                         └──────┘                        └───────────┘          └──┘      └───────────┘       └──┘         └───────────┘     └───────────┘
typ                                         └──────┘  └┘         └┘ └┘   └───────────┘ └┘  └┘  └──┘     └───────────┘ └┘   └──┘   └┘   └───────────┘ └┘  └───────────┘     └┘ └┘
124  begin
st   └─────
125    induction t; simp!; intros; is_searchable_tactic,
id                                └──────────────────┘
src    └────────┘   └───┘  └────┘  └──────────────────┘
typ    └────────┘  └───┘  └────┘  └──────────────────┘
doc    └────────┘   └───┘  └────┘
txt    └────────┘   └───┘  └────┘
par    └────────┘   └───┘  └────┘  └──────────────────┘
pid                    
st   ─────────────────────────────────────────────────┘└─
126    { cases hi,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└──────┘└─
127      { apply is_searchable_none_high_of_is_searchable_some_high, assumption },
id               └────────────────────────────────────────────────┘
src        └────┘└────────────────────────────────────────────────┘  └─────────┘
typ        └────┘└────────────────────────────────────────────────┘  └─────────┘
doc        └────┘                                                    └─────────┘
txt        └────┘                                                    └─────────┘
par        └────┘                                                    └─────────┘
pid                                                                           
st   ─────┘└──────────────────────────────────────────────────────┘└───────────┘└┘
128      { simp at *, apply is_searchable_some_high_of_is_searchable_of_lt, assumption' } },
id                          └────────────────────────────────────────────┘
src        └───────┘  └────┘└────────────────────────────────────────────┘  └──────────┘
typ        └───────┘  └────┘└────────────────────────────────────────────┘  └──────────┘
doc        └───────┘  └────┘                                                └──────────┘
txt        └───────┘  └────┘                                                └──────────┘
par        └───────┘  └────┘                                                └──────────┘
pid            └──┘                                                                  
st   ──────────────┘└────────────────────────────────────────────────────┘└────────────┘└──┘
129    all_goals { apply is_searchable_balance2, assumption' }
id                       └────────────────────┘
src    └──────────┘└────┘└────────────────────┘└┘└──────────┘└┘
typ    └──────────┘└────┘└────────────────────┘└┘└──────────┘└┘
doc    └──────────┘└────┘                      └┘└──────────┘└┘
txt    └──────────┘└────┘                      └┘└──────────┘└┘
par    └──────────┘└────┘                      └┘└──────────┘└┘
pid             └───────┘                      └─────────────┘
st   ────────────┘└───────────────────────────┘└────────────┘
130  end
st   └─┘
131  
132  lemma is_searchable_ins {t x} [is_strict_weak_order α lt] : ∀ {lo hi} (h : is_searchable lt t lo hi), lift lt lo (some x) → lift lt (some x) hi → is_searchable lt (ins lt t x) lo hi :=
id                                  └──────────────────┘  └┘       └┘ └┘       └───────────┘ └┘  └┘ └┘   └──┘ └┘ └┘  └──┘     └──┘ └┘  └──┘   └┘   └───────────┘ └┘  └─┘ └┘    └┘ └┘
src                                 └──────────────────┘                        └───────────┘              └──┘        └──┘      └──┘     └──┘         └───────────┘     └─┘
typ                                 └──────────────────┘  └┘       └┘ └┘       └───────────┘ └┘  └┘ └┘   └──┘ └┘ └┘  └──┘     └──┘ └┘  └──┘   └┘   └───────────┘ └┘  └─┘ └┘    └┘ └┘
133  begin
st   └─────
134    with_cases { apply ins.induction lt t x; intros; simp! [*] at * {eta := ff}; is_searchable_tactic },
id                        └───────────┘ └┘                                   └┘   └──────────────────┘
src    └───────────┘└────┘└───────────┘    └┘└────┘└┘└─────────────┘ └─────┘└┘└┘└──────────────────┘└┘
typ    └───────────┘└────┘└───────────┘└┘└┘└────┘└┘└─────────────┘ └─────┘└┘└┘└──────────────────┘└┘
doc    └───────────┘└────┘                 └┘└────┘└┘└─────────────┘ └─────┘  └┘                    └┘
txt    └───────────┘└────┘                 └┘└────┘└┘└─────────────┘ └─────┘  └┘                    └┘
par    └───────────┘└────┘                 └┘└────┘└┘└─────────────┘ └─────┘  └┘└──────────────────┘└┘
pid              └───────┘                 └───────────────────────┘ └─────┘  └─┘                    └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────┘└─┘
135    case is_red_lt { apply ih h_hs₁, assumption, simp [*] },
id                            └┘ └───┘
src    └───────────────┘└────┘       └┘└────────┘└┘└───────┘
typ    └───────────────┘└────┘└┘└───┘└┘└────────┘└┘└───────┘
doc    └───────────────┘└────┘       └┘└────────┘└┘└───────┘
txt    └───────────────┘└────┘       └┘└────────┘└┘└───────┘
par    └───────────────┘└────┘       └┘└────────┘└┘└───────┘
pid        └────────┘└──────┘       └──────────────────────┘
st   ─────────────────┘└─────────────┘└──────────┘└─────────┘└┘
136    case is_red_eq hs₁ { apply is_searchable_of_is_searchable_of_incomp hc, assumption },
id                                └──────────────────────────────────────┘ └┘
src    └───────────────────┘└────┘└──────────────────────────────────────┘  └┘└─────────┘
typ    └───────────────────┘└────┘└──────────────────────────────────────┘└┘└┘└─────────┘
doc    └───────────────────┘└────┘                                          └┘└─────────┘
txt    └───────────────────┘└────┘                                          └┘└─────────┘
par    └───────────────────┘└────┘                                          └┘└─────────┘
pid        └────────────┘└──────┘                                          └────────────┘
st   ─────────────────────┘└────────────────────────────────────────────────┘└───────────┘└┘
137    case is_red_eq hs₂ { apply is_searchable_of_incomp_of_is_searchable hc, assumption },
id                                └──────────────────────────────────────┘ └┘
src    └───────────────────┘└────┘└──────────────────────────────────────┘  └┘└─────────┘
typ    └───────────────────┘└────┘└──────────────────────────────────────┘└┘└┘└─────────┘
doc    └───────────────────┘└────┘                                          └┘└─────────┘
txt    └───────────────────┘└────┘                                          └┘└─────────┘
par    └───────────────────┘└────┘                                          └┘└─────────┘
pid        └────────────┘└──────┘                                          └────────────┘
st   ─────────────────────┘└────────────────────────────────────────────────┘└───────────┘└┘
138    case is_red_gt { apply ih h_hs₂, cases hi; simp [*], assumption },
id                            └┘ └───┘        └┘
src    └───────────────┘└────┘       └┘└────┘  └┘└──────┘└┘└─────────┘
typ    └───────────────┘└────┘└┘└───┘└┘└────┘└┘└┘└──────┘└┘└─────────┘
doc    └───────────────┘└────┘       └┘└────┘  └┘└──────┘└┘└─────────┘
txt    └───────────────┘└────┘       └┘└────┘  └┘└──────┘└┘└─────────┘
par    └───────────────┘└────┘       └┘└────┘  └┘└──────┘└┘└─────────┘
pid        └────────┘└──────┘       └──────┘  └──────────────────────┘
st   ─────────────────┘└─────────────┘└──────────────────┘└───────────┘└┘
139    case is_black_lt_red { apply is_searchable_balance1_node, apply ih h_hs₁, assumption, simp [*], assumption },
id                                  └─────────────────────────┘        └┘ └───┘
src    └─────────────────────┘└────┘└─────────────────────────┘└┘└────┘       └┘└────────┘└┘└──────┘└┘└─────────┘
typ    └─────────────────────┘└────┘└─────────────────────────┘└┘└────┘└┘└───┘└┘└────────┘└┘└──────┘└┘└─────────┘
doc    └─────────────────────┘└────┘                           └┘└────┘       └┘└────────┘└┘└──────┘└┘└─────────┘
txt    └─────────────────────┘└────┘                           └┘└────┘       └┘└────────┘└┘└──────┘└┘└─────────┘
par    └─────────────────────┘└────┘                           └┘└────┘       └┘└────────┘└┘└──────┘└┘└─────────┘
pid        └──────────────┘└──────┘                           └──────┘       └──────────────────────────────────┘
st   ───────────────────────┘└────────────────────────────────┘└──────────────┘└──────────┘└────────┘└───────────┘└┘
140    case is_black_lt_not_red { apply ih h_hs₁, assumption, simp [*] },
id                                      └┘ └───┘
src    └─────────────────────────┘└────┘       └┘└────────┘└┘└───────┘
typ    └─────────────────────────┘└────┘└┘└───┘└┘└────────┘└┘└───────┘
doc    └─────────────────────────┘└────┘       └┘└────────┘└┘└───────┘
txt    └─────────────────────────┘└────┘       └┘└────────┘└┘└───────┘
par    └─────────────────────────┘└────┘       └┘└────────┘└┘└───────┘
pid        └──────────────────┘└──────┘       └──────────────────────┘
st   ───────────────────────────┘└─────────────┘└──────────┘└─────────┘└┘
141    case is_black_eq hs₁ { apply is_searchable_of_is_searchable_of_incomp hc, assumption },
id                                  └──────────────────────────────────────┘ └┘
src    └─────────────────────┘└────┘└──────────────────────────────────────┘  └┘└─────────┘
typ    └─────────────────────┘└────┘└──────────────────────────────────────┘└┘└┘└─────────┘
doc    └─────────────────────┘└────┘                                          └┘└─────────┘
txt    └─────────────────────┘└────┘                                          └┘└─────────┘
par    └─────────────────────┘└────┘                                          └┘└─────────┘
pid        └──────────────┘└──────┘                                          └────────────┘
st   ───────────────────────┘└────────────────────────────────────────────────┘└───────────┘└┘
142    case is_black_eq hs₂ { apply is_searchable_of_incomp_of_is_searchable hc, assumption },
id                                  └──────────────────────────────────────┘ └┘
src    └─────────────────────┘└────┘└──────────────────────────────────────┘  └┘└─────────┘
typ    └─────────────────────┘└────┘└──────────────────────────────────────┘└┘└┘└─────────┘
doc    └─────────────────────┘└────┘                                          └┘└─────────┘
txt    └─────────────────────┘└────┘                                          └┘└─────────┘
par    └─────────────────────┘└────┘                                          └┘└─────────┘
pid        └──────────────┘└──────┘                                          └────────────┘
st   ───────────────────────┘└────────────────────────────────────────────────┘└───────────┘└┘
143    case is_black_gt_red { apply is_searchable_balance2_node, assumption, apply ih h_hs₂, simp [*], assumption },
id                                  └─────────────────────────┘                    └┘ └───┘
src    └─────────────────────┘└────┘└─────────────────────────┘└┘└────────┘└┘└────┘       └┘└──────┘└┘└─────────┘
typ    └─────────────────────┘└────┘└─────────────────────────┘└┘└────────┘└┘└────┘└┘└───┘└┘└──────┘└┘└─────────┘
doc    └─────────────────────┘└────┘                           └┘└────────┘└┘└────┘       └┘└──────┘└┘└─────────┘
txt    └─────────────────────┘└────┘                           └┘└────────┘└┘└────┘       └┘└──────┘└┘└─────────┘
par    └─────────────────────┘└────┘                           └┘└────────┘└┘└────┘       └┘└──────┘└┘└─────────┘
pid        └──────────────┘└──────┘                           └──────────────────┘       └──────────────────────┘
st   ───────────────────────┘└────────────────────────────────┘└──────────┘└──────────────┘└────────┘└───────────┘└┘
144    case is_black_gt_not_red { apply ih h_hs₂, assumption, simp [*] }
id                                      └┘ └───┘
src    └─────────────────────────┘└────┘       └┘└────────┘└┘└───────┘└┘
typ    └─────────────────────────┘└────┘└┘└───┘└┘└────────┘└┘└───────┘└┘
doc    └─────────────────────────┘└────┘       └┘└────────┘└┘└───────┘└┘
txt    └─────────────────────────┘└────┘       └┘└────────┘└┘└───────┘└┘
par    └─────────────────────────┘└────┘       └┘└────────┘└┘└───────┘└┘
pid        └──────────────────┘└──────┘       └──────────────────────┘
st   ───────────────────────────┘└─────────────┘└──────────┘└─────────┘
145  end
st   └─┘
146  
147  lemma is_searchable_mk_insert_result {c t} : is_searchable lt t none none → is_searchable lt (mk_insert_result c t) none none :=
id                                                └───────────┘ └┘  └──┘ └──┘   └───────────┘ └┘  └──────────────┘    └──┘ └──┘
src                                               └───────────┘      └──┘ └──┘   └───────────┘     └──────────────┘      └──┘ └──┘
typ                                               └───────────┘ └┘  └──┘ └──┘   └───────────┘ └┘  └──────────────┘    └──┘ └──┘
148  begin
st   └─────
149    cases c; cases t; simp [mk_insert_result],
id                           └──────────────┘
src    └────┘   └────┘   └────┘└──────────────┘
typ    └────┘  └────┘  └────┘└──────────────┘
doc    └────┘   └────┘   └────┘                
txt    └────┘   └────┘   └────┘                
par    └────┘   └────┘   └────┘                
pid                                        
st   ──────────────────────────────────────────┘└─
150    any_goals { exact id },
id                       └┘
src    └──────────┘└────┘└┘
typ    └──────────┘└────┘└┘
doc    └──────────┘└────┘  
txt    └──────────┘└────┘  
par    └──────────┘└────┘  
pid             └───────┘  └┘
st   ────────────┘└────────┘└┘
151    { intro h, is_searchable_tactic }
id                └──────────────────┘
src      └─────┘  └──────────────────┘
typ      └─────┘  └──────────────────┘
doc      └─────┘
txt      └─────┘
par      └─────┘  └──────────────────┘
pid           └┘
st   ──────────┘└────────────────────┘└──
152  end
st   ──┘
153  
154  lemma is_searchable_insert {t x} [is_strict_weak_order α lt] : is_searchable lt t none none → is_searchable lt (insert lt t x) none none :=
id                                     └──────────────────┘  └┘    └───────────┘ └┘  └──┘ └──┘   └───────────┘ └┘  └────┘ └┘    └──┘ └──┘
src                                    └──────────────────┘         └───────────┘      └──┘ └──┘   └───────────┘     └────┘         └──┘ └──┘
typ                                    └──────────────────┘  └┘    └───────────┘ └┘  └──┘ └──┘   └───────────┘ └┘  └────┘ └┘    └──┘ └──┘
155  begin
st   └─────
156    intro h, simp [insert], apply is_searchable_mk_insert_result, apply is_searchable_ins; { assumption <|> simp }
id                    └────┘         └────────────────────────────┘        └───────────────┘
src    └─────┘  └────┘└────┘  └────┘└────────────────────────────┘  └────┘└───────────────┘    └─────────┘    └───┘
typ    └─────┘  └────┘└────┘  └────┘└────────────────────────────┘  └────┘└───────────────┘    └─────────┘    └───┘
doc    └─────┘  └────┘        └────┘                                └────┘                     └─────────┘    └───┘
txt    └─────┘  └────┘        └────┘                                └────┘                     └─────────┘    └───┘
par    └─────┘  └────┘        └────┘                                └────┘                     └─────────┘    └───┘
pid         └┘                                                                                               
st   ────────┘└─────────────┘└────────────────────────────────────┘└─────────────────────────┘└────────────────────┘└─
157  end
st   ──┘
158  
159  end rbnode
160  
161  namespace rbnode
162  section membership_lemmas
163  parameters {α : Type u} (lt : α → α → Prop) [decidable_rel lt]
id                                               └───────────┘
src                                               └───────────┘
typ                                              └───────────┘
164  
165  local attribute [simp] mem balance1_node balance2_node
id                          └─┘ └───────────┘ └───────────┘
src                         └─┘ └───────────┘ └───────────┘
typ                         └─┘ └───────────┘ └───────────┘
doc                   └──┘
166  
167  local infix `∈` := mem lt
id                      └─┘
src                     └─┘
typ                     └─┘
168  
169  lemma mem_balance1_node_of_mem_left {x s} (v) (t : rbnode α) : x ∈ s → x ∈ balance1_node s v t :=
id                                                      └────┘            └───────────┘   
src                                                     └────┘                └───────────┘
typ                                                     └────┘            └───────────┘   
170  begin
st   └─────
171    cases s; simp,
id           
src    └────┘   └──┘
typ    └────┘  └──┘
doc    └────┘   └──┘
txt    └────┘   └──┘
par    └────┘   └──┘
pid         
st   ──────────────┘└─
172    all_goals { apply balance.cases s_lchild s_val s_rchild; intros; simp at *; blast_disjs; simp [*] }
id                       └───────────┘ └──────┘ └───┘ └──────┘
src    └──────────┘└────┘└───────────┘                     └┘└────┘└┘└───────┘└┘└─────────┘└┘└───────┘└┘
typ    └──────────┘└────┘└───────────┘└──────┘└───┘└──────┘└┘└────┘└┘└───────┘└┘└─────────┘└┘└───────┘└┘
doc    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘           └┘└───────┘└┘
txt    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘└─────────┘└┘└───────┘└┘
par    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘└─────────┘└┘└───────┘└┘
pid             └───────┘                                  └──────────────────────────────────────────┘
st   ────────────┘└─────────────────────────────────────────────────────────────────────────────────────┘
173  end
st   └─┘
174  
175  lemma mem_balance2_node_of_mem_left {x s} (v) (t : rbnode α) : x ∈ s → x ∈ balance2_node s v t :=
id                                                      └────┘            └───────────┘   
src                                                     └────┘                └───────────┘
typ                                                     └────┘            └───────────┘   
176  begin
st   └─────
177    cases s; simp,
id           
src    └────┘   └──┘
typ    └────┘  └──┘
doc    └────┘   └──┘
txt    └────┘   └──┘
par    └────┘   └──┘
pid         
st   ──────────────┘└─
178    all_goals { apply balance.cases s_lchild s_val s_rchild; intros; simp at *; blast_disjs; simp [*] }
id                       └───────────┘ └──────┘ └───┘ └──────┘
src    └──────────┘└────┘└───────────┘                     └┘└────┘└┘└───────┘└┘└─────────┘└┘└───────┘└┘
typ    └──────────┘└────┘└───────────┘└──────┘└───┘└──────┘└┘└────┘└┘└───────┘└┘└─────────┘└┘└───────┘└┘
doc    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘           └┘└───────┘└┘
txt    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘└─────────┘└┘└───────┘└┘
par    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘└─────────┘└┘└───────┘└┘
pid             └───────┘                                  └──────────────────────────────────────────┘
st   ────────────┘└─────────────────────────────────────────────────────────────────────────────────────┘
179  end
st   └─┘
180  
181  lemma mem_balance1_node_of_mem_right {x t} (v) (s : rbnode α) : x ∈ t → x ∈ balance1_node s v t :=
id                                                       └────┘            └───────────┘   
src                                                      └────┘                └───────────┘
typ                                                      └────┘            └───────────┘   
182  begin
st   └─────
183    intros, cases s; simp [*],
id                   
src    └────┘  └────┘   └──────┘
typ    └────┘  └────┘  └──────┘
doc    └────┘  └────┘   └──────┘
txt    └────┘  └────┘   └──────┘
par    └────┘  └────┘   └──────┘
pid                        └─┘
st   ───────┘└─────────────────┘└─
184    all_goals { apply balance.cases s_lchild s_val s_rchild; intros; simp [*] }
id                       └───────────┘ └──────┘ └───┘ └──────┘
src    └──────────┘└────┘└───────────┘                     └┘└────┘└┘└───────┘└┘
typ    └──────────┘└────┘└───────────┘└──────┘└───┘└──────┘└┘└────┘└┘└───────┘└┘
doc    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
txt    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
par    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
pid             └───────┘                                  └──────────────────┘
st   ────────────┘└─────────────────────────────────────────────────────────────┘
185  end
st   └─┘
186  
187  lemma mem_balance2_node_of_mem_right {x t} (v) (s : rbnode α) : x ∈ t → x ∈ balance2_node s v t :=
id                                                       └────┘            └───────────┘   
src                                                      └────┘                └───────────┘
typ                                                      └────┘            └───────────┘   
188  begin
st   └─────
189    intros, cases s; simp [*],
id                   
src    └────┘  └────┘   └──────┘
typ    └────┘  └────┘  └──────┘
doc    └────┘  └────┘   └──────┘
txt    └────┘  └────┘   └──────┘
par    └────┘  └────┘   └──────┘
pid                        └─┘
st   ───────┘└─────────────────┘└─
190    all_goals { apply balance.cases s_lchild s_val s_rchild; intros; simp [*] }
id                       └───────────┘ └──────┘ └───┘ └──────┘
src    └──────────┘└────┘└───────────┘                     └┘└────┘└┘└───────┘└┘
typ    └──────────┘└────┘└───────────┘└──────┘└───┘└──────┘└┘└────┘└┘└───────┘└┘
doc    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
txt    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
par    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
pid             └───────┘                                  └──────────────────┘
st   ────────────┘└─────────────────────────────────────────────────────────────┘
191  end
st   └─┘
192  
193  lemma mem_balance1_node_of_incomp {x v} (s t) : (¬ lt x v ∧ ¬ lt v x) → s ≠ leaf → x ∈ balance1_node s v t :=
id                                                     └┘     └┘        └──┘     └───────────┘   
src                                                                          └──┘      └───────────┘
typ                                                    └┘     └┘        └──┘     └───────────┘   
194  begin
st   └─────
195    intros, cases s; simp,
id                   
src    └────┘  └────┘   └──┘
typ    └────┘  └────┘  └──┘
doc    └────┘  └────┘   └──┘
txt    └────┘  └────┘   └──┘
par    └────┘  └────┘   └──┘
pid                 
st   ───────┘└─────────────┘└─
196    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
197    all_goals { apply balance.cases s_lchild s_val s_rchild; intros; simp [*] }
id                       └───────────┘ └──────┘ └───┘ └──────┘
src    └──────────┘└────┘└───────────┘                     └┘└────┘└┘└───────┘└┘
typ    └──────────┘└────┘└───────────┘└──────┘└───┘└──────┘└┘└────┘└┘└───────┘└┘
doc    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
txt    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
par    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
pid             └───────┘                                  └──────────────────┘
st   ────────────┘└─────────────────────────────────────────────────────────────┘
198  end
st   └─┘
199  
200  lemma mem_balance2_node_of_incomp {x v} (s t) : (¬ lt v x ∧ ¬ lt x v) → s ≠ leaf → x ∈ balance2_node s v t :=
id                                                     └┘     └┘        └──┘     └───────────┘   
src                                                                          └──┘      └───────────┘
typ                                                    └┘     └┘        └──┘     └───────────┘   
201  begin
st   └─────
202    intros, cases s; simp,
id                   
src    └────┘  └────┘   └──┘
typ    └────┘  └────┘  └──┘
doc    └────┘  └────┘   └──┘
txt    └────┘  └────┘   └──┘
par    └────┘  └────┘   └──┘
pid                 
st   ───────┘└─────────────┘└─
203    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
204    all_goals { apply balance.cases s_lchild s_val s_rchild; intros; simp [*] }
id                       └───────────┘ └──────┘ └───┘ └──────┘
src    └──────────┘└────┘└───────────┘                     └┘└────┘└┘└───────┘└┘
typ    └──────────┘└────┘└───────────┘└──────┘└───┘└──────┘└┘└────┘└┘└───────┘└┘
doc    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
txt    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
par    └──────────┘└────┘                                  └┘└────┘└┘└───────┘└┘
pid             └───────┘                                  └──────────────────┘
st   ────────────┘└─────────────────────────────────────────────────────────────┘
205  end
st   └─┘
206  
207  lemma ins_ne_leaf (t : rbnode α) (x : α) : t.ins lt x ≠ leaf :=
id                          └────┘            └──┘ └┘   └──┘
src                         └────┘               └──┘       └──┘
typ                         └────┘            └──┘ └┘   └──┘
208  begin
st   └─────
209    apply ins.induction lt t x,
id           └───────────┘ └┘  
src    └────┘└───────────┘   
typ    └────┘└───────────┘└┘
doc    └────┘                
txt    └────┘                
par    └────┘                
pid                         
st   ───────────────────────────┘└─
210    any_goals { intros, simp [ins, *] },
id                               └─┘
src    └──────────┘└────┘└┘└────┘└─┘└───┘
typ    └──────────┘└────┘└┘└────┘└─┘└───┘
doc    └──────────┘└────┘└┘└────┘   └───┘
txt    └──────────┘└────┘└┘└────┘   └───┘
par    └──────────┘└────┘└┘└────┘   └───┘
pid             └───────────────┘   └────┘
st   ────────────┘└─────────────────────┘└┘
211    { intros, apply balance1_node_ne_leaf, assumption },
id                     └───────────────────┘
src      └────┘  └────┘└───────────────────┘  └─────────┘
typ      └────┘  └────┘└───────────────────┘  └─────────┘
doc      └────┘  └────┘                       └─────────┘
txt      └────┘  └────┘                       └─────────┘
par      └────┘  └────┘                       └─────────┘
pid                                                    
st   ───┘└─────────────────────────────────┘└───────────┘└┘
212    { intros, apply balance2_node_ne_leaf, assumption },
id                     └───────────────────┘
src      └────┘  └────┘└───────────────────┘  └─────────┘
typ      └────┘  └────┘└───────────────────┘  └─────────┘
doc      └────┘  └────┘                       └─────────┘
txt      └────┘  └────┘                       └─────────┘
par      └────┘  └────┘                       └─────────┘
pid                                                    
st   ──────────────────────────────────────┘└───────────┘└──
213  end
st   ──┘
214  
215  lemma insert_ne_leaf (t : rbnode α) (x : α) : insert lt t x ≠ leaf :=
id                             └────┘            └────┘ └┘    └──┘
src                            └────┘              └────┘         └──┘
typ                            └────┘            └────┘ └┘    └──┘
216  begin
st   └─────
217    simp [insert],
id           └────┘
src    └────┘└────┘
typ    └────┘└────┘
doc    └────┘      
txt    └────┘      
par    └────┘      
pid              
st   ──────────────┘└─
218    cases he : ins lt t x; cases get_color t; simp [mk_insert_result],
id                └─┘ └┘          └───────┘         └──────────────┘
src    └────┘  └─┘└─┘      └────┘└───────┘   └────┘└──────────────┘
typ    └────┘  └─┘└─┘└┘  └────┘└───────┘  └────┘└──────────────┘
doc    └────┘  └─┘         └────┘            └────┘                
txt    └────┘  └─┘         └────┘            └────┘                
par    └────┘  └─┘         └────┘            └────┘                
pid           └─┘                                              
st   ──────────────────────────────────────────────────────────────────┘└─
219    { have := ins_ne_leaf lt t x, contradiction },
id               └─────────┘ └┘  
src      └──────┘└─────────┘      └────────────┘
typ      └──────┘└─────────┘└┘  └────────────┘
doc      └──────┘                 └────────────┘
txt      └──────┘                 └────────────┘
par      └──────┘                 └────────────┘
pid      └───┘└─┘                              
st   ───┘└────────────────────────┘└──────────────┘└┘
220    { exact absurd he (ins_ne_leaf _ _ _) }
id             └────┘ └┘  └─────────┘
src      └────┘└────┘   └─────────┘└──────┘
typ      └────┘└────┘└┘ └─────────┘└──────┘
doc      └────┘                    └──────┘
txt      └────┘                    └──────┘
par      └────┘                    └──────┘
pid                               └─────┘
st   ───────────────────────────────────────┘└─
221  end
st   ──┘
222  
223  lemma mem_ins_of_incomp (t : rbnode α) {x y : α} : ∀ h : ¬ lt x y ∧ ¬ lt y x, x ∈ t.ins lt y :=
id                                └────┘                     └┘     └┘      └──┘ └┘ 
src                               └────┘                                            └──┘
typ                               └────┘                     └┘     └┘      └──┘ └┘ 
224  begin
st   └─────
225    with_cases { apply ins.induction lt t y; intros; simp [ins, *] },
id                        └───────────┘ └┘                  └─┘
src    └───────────┘└────┘└───────────┘    └┘└────┘└┘└────┘└─┘└───┘
typ    └───────────┘└────┘└───────────┘└┘└┘└────┘└┘└────┘└─┘└───┘
doc    └───────────┘└────┘                 └┘└────┘└┘└────┘   └───┘
txt    └───────────┘└────┘                 └┘└────┘└┘└────┘   └───┘
par    └───────────┘└────┘                 └┘└────┘└┘└────┘   └───┘
pid              └───────┘                 └──────────────┘   └────┘
st   ────────────────────────────────────────────────────────────────┘└┘
226    case is_black_lt_red { have := ih h, apply mem_balance1_node_of_mem_left, assumption },
id                                    └┘         └───────────────────────────┘
src    └─────────────────────┘└──────┘   └┘└────┘└───────────────────────────┘└┘└─────────┘
typ    └─────────────────────┘└──────┘└┘└┘└────┘└───────────────────────────┘└┘└─────────┘
doc    └─────────────────────┘└──────┘   └┘└────┘                             └┘└─────────┘
txt    └─────────────────────┘└──────┘   └┘└────┘                             └┘└─────────┘
par    └─────────────────────┘└──────┘   └┘└────┘                             └┘└─────────┘
pid        └──────────────┘└────────┘   └──────┘                             └────────────┘
st   ───────────────────────┘└───────────┘└───────────────────────────────────┘└───────────┘└┘
227    case is_black_gt_red { have := ih h, apply mem_balance2_node_of_mem_left, assumption }
id                                    └┘         └───────────────────────────┘
src    └─────────────────────┘└──────┘   └┘└────┘└───────────────────────────┘└┘└─────────┘└┘
typ    └─────────────────────┘└──────┘└┘└┘└────┘└───────────────────────────┘└┘└─────────┘└┘
doc    └─────────────────────┘└──────┘   └┘└────┘                             └┘└─────────┘└┘
txt    └─────────────────────┘└──────┘   └┘└────┘                             └┘└─────────┘└┘
par    └─────────────────────┘└──────┘   └┘└────┘                             └┘└─────────┘└┘
pid        └──────────────┘└────────┘   └──────┘                             └────────────┘
st   ───────────────────────┘└───────────┘└───────────────────────────────────┘└───────────┘
228  end
st   └─┘
229  
230  lemma mem_ins_of_mem [is_strict_weak_order α lt] {t : rbnode α} (z : α) : ∀ {x} (h : x ∈ t), x ∈ t.ins lt z :=
id                         └──────────────────┘  └┘       └────┘                             └──┘ └┘ 
src                        └──────────────────┘            └────┘                                    └──┘
typ                        └──────────────────┘  └┘       └────┘                             └──┘ └┘ 
231  begin
st   └─────
232    with_cases { apply ins.induction lt t z; intros; simp [ins, *] at *; try { contradiction }; blast_disjs },
id                        └───────────┘ └┘                  └─┘
src    └───────────┘└────┘└───────────┘    └┘└────┘└┘└────┘└─┘└───────┘└┘└────┘└────────────┘└┘└──────────┘
typ    └───────────┘└────┘└───────────┘└┘└┘└────┘└┘└────┘└─┘└───────┘└──────┘└────────────┘└─┘└──────────┘
doc    └───────────┘└────┘                 └┘└────┘└┘└────┘   └───────┘└┘└────┘└────────────┘└┘            
txt    └───────────┘└────┘                 └┘└────┘└┘└────┘   └───────┘└┘└────┘└────────────┘└┘└──────────┘
par    └───────────┘└────┘                 └┘└────┘└┘└────┘   └───────┘└──────┘└────────────┘└─┘└──────────┘
pid              └───────┘                 └──────────────┘   └─────────────────────────────────────────────┘
st   ───────────────────────────────────────────────────────────────────────────┘└─────────────┘ └────────────┘└┘
233    case is_red_eq or.inr or.inl {
src    └──────────────────────────────
typ    └──────────────────────────────
doc    └──────────────────────────────
txt    └──────────────────────────────
par    └──────────────────────────────
pid        └──────────────────────┘└─
st   ───────────────────────────────┘
234      have := incomp_trans_of lt h ⟨hc.2, hc.1⟩, simp [this] },
id               └─────────────┘ └┘         └┘           └──┘
src  ───┘└──────┘└─────────────┘      └──┘  └─┘└┘└────┘    └┘
typ  ───┘└──────┘└─────────────┘└┘   └──┘└┘└─┘└┘└────┘└──┘└┘
doc  ───┘└──────┘                     └──┘  └─┘└┘└────┘    └┘
txt  ───┘└──────┘                     └──┘  └─┘└┘└────┘    └┘
par  ───┘└──────┘                     └──┘  └─┘└┘└────┘    └┘
pid  ───────────┘                     └──┘  └─────────┘    └─┘
st   ────────────────────────────────────────────┘└────────────┘└┘
235    case is_black_lt_red or.inl {
src    └─────────────────────────────
typ    └─────────────────────────────
doc    └─────────────────────────────
txt    └─────────────────────────────
par    └─────────────────────────────
pid        └─────────────────────┘└─
st   ──────────────────────────────┘
236      apply mem_balance1_node_of_mem_left, apply ih h },
id             └───────────────────────────┘        └┘ 
src  ───┘└────┘└───────────────────────────┘└┘└────┘   
typ  ───┘└────┘└───────────────────────────┘└┘└────┘└┘
doc  ───┘└────┘                             └┘└────┘   
txt  ───┘└────┘                             └┘└────┘   
par  ───┘└────┘                             └┘└────┘   
pid  ─────────┘                             └──────┘   └┘
st   ──────────────────────────────────────┘└───────────┘└┘
237    case is_black_lt_red or.inr or.inl {
src    └────────────────────────────────────
typ    └────────────────────────────────────
doc    └────────────────────────────────────
txt    └────────────────────────────────────
par    └────────────────────────────────────
pid        └────────────────────────────┘└─
st   ─────────────────────────────────────┘
238      have := ins_ne_leaf lt a z, apply mem_balance1_node_of_incomp, cases h, all_goals { simp [*] } },
id               └─────────┘ └┘          └─────────────────────────┘        
src  ───┘└──────┘└─────────┘    └┘└────┘└─────────────────────────┘└┘└────┘ └┘└──────────┘└───────┘└┘
typ  ───┘└──────┘└─────────┘└┘└┘└────┘└─────────────────────────┘└┘└────┘└┘└──────────┘└───────┘└┘
doc  ───┘└──────┘               └┘└────┘                           └┘└────┘ └┘└──────────┘└───────┘└┘
txt  ───┘└──────┘               └┘└────┘                           └┘└────┘ └┘└──────────┘└───────┘└┘
par  ───┘└──────┘               └┘└────┘                           └┘└────┘ └┘└──────────┘└───────┘└┘
pid  ───────────┘               └──────┘                           └──────┘ └────────────────────────┘
st   ─────────────────────────────┘└─────────────────────────────────┘└───────┘└───────────┘└────────┘└┘
239    case is_black_lt_red or.inr or.inr {
src    └────────────────────────────────────
typ    └────────────────────────────────────
doc    └────────────────────────────────────
txt    └────────────────────────────────────
par    └────────────────────────────────────
pid        └────────────────────────────┘└─
st   ─────────────────────────────────────┘
240      apply mem_balance1_node_of_mem_right, assumption },
id             └────────────────────────────┘
src  ───┘└────┘└────────────────────────────┘└┘└─────────┘
typ  ───┘└────┘└────────────────────────────┘└┘└─────────┘
doc  ───┘└────┘                              └┘└─────────┘
txt  ───┘└────┘                              └┘└─────────┘
par  ───┘└────┘                              └┘└─────────┘
pid  ─────────┘                              └────────────┘
st   ───────────────────────────────────────┘└───────────┘└┘
241    case is_black_eq or.inr or.inl {
src    └────────────────────────────────
typ    └────────────────────────────────
doc    └────────────────────────────────
txt    └────────────────────────────────
par    └────────────────────────────────
pid        └────────────────────────┘└─
st   ─────────────────────────────────┘
242      have := incomp_trans_of lt hc ⟨h.2, h.1⟩, simp [this] },
id               └─────────────┘ └┘ └┘                  └──┘
src  ───┘└──────┘└─────────────┘      └──┘ └─┘└┘└────┘    └┘
typ  ───┘└──────┘└─────────────┘└┘└┘  └──┘└─┘└┘└────┘└──┘└┘
doc  ───┘└──────┘                     └──┘ └─┘└┘└────┘    └┘
txt  ───┘└──────┘                     └──┘ └─┘└┘└────┘    └┘
par  ───┘└──────┘                     └──┘ └─┘└┘└────┘    └┘
pid  ───────────┘                     └──┘ └─────────┘    └─┘
st   ───────────────────────────────────────────┘└────────────┘└┘
243    case is_black_gt_red or.inl {
src    └─────────────────────────────
typ    └─────────────────────────────
doc    └─────────────────────────────
txt    └─────────────────────────────
par    └─────────────────────────────
pid        └─────────────────────┘└─
st   ──────────────────────────────┘
244      apply mem_balance2_node_of_mem_right, assumption },
id             └────────────────────────────┘
src  ───┘└────┘└────────────────────────────┘└┘└─────────┘
typ  ───┘└────┘└────────────────────────────┘└┘└─────────┘
doc  ───┘└────┘                              └┘└─────────┘
txt  ───┘└────┘                              └┘└─────────┘
par  ───┘└────┘                              └┘└─────────┘
pid  ─────────┘                              └────────────┘
st   ───────────────────────────────────────┘└───────────┘└┘
245    case is_black_gt_red or.inr or.inl {
src    └────────────────────────────────────
typ    └────────────────────────────────────
doc    └────────────────────────────────────
txt    └────────────────────────────────────
par    └────────────────────────────────────
pid        └────────────────────────────┘└─
st   ─────────────────────────────────────┘
246      have := ins_ne_leaf lt a z, apply mem_balance2_node_of_incomp, cases h, simp [*], apply ins_ne_leaf },
id               └─────────┘ └┘          └─────────────────────────┘                          └─────────┘
src  ───┘└──────┘└─────────┘    └┘└────┘└─────────────────────────┘└┘└────┘ └┘└──────┘└┘└────┘└─────────┘
typ  ───┘└──────┘└─────────┘└┘└┘└────┘└─────────────────────────┘└┘└────┘└┘└──────┘└┘└────┘└─────────┘
doc  ───┘└──────┘               └┘└────┘                           └┘└────┘ └┘└──────┘└┘└────┘           
txt  ───┘└──────┘               └┘└────┘                           └┘└────┘ └┘└──────┘└┘└────┘           
par  ───┘└──────┘               └┘└────┘                           └┘└────┘ └┘└──────┘└┘└────┘           
pid  ───────────┘               └──────┘                           └──────┘ └────────────────┘           └┘
st   ─────────────────────────────┘└─────────────────────────────────┘└───────┘└────────┘└──────────────────┘└┘
247    case is_black_gt_red or.inr or.inr {
src    └────────────────────────────────────
typ    └────────────────────────────────────
doc    └────────────────────────────────────
txt    └────────────────────────────────────
par    └────────────────────────────────────
pid        └────────────────────────────┘└─
st   ─────────────────────────────────────┘
248      apply mem_balance2_node_of_mem_left, apply ih h },
id             └───────────────────────────┘        └┘ 
src  ───┘└────┘└───────────────────────────┘└┘└────┘   
typ  ───┘└────┘└───────────────────────────┘└┘└────┘└┘
doc  ───┘└────┘                             └┘└────┘   
txt  ───┘└────┘                             └┘└────┘   
par  ───┘└────┘                             └┘└────┘   
pid  ─────────┘                             └──────┘   └┘
st   ──────────────────────────────────────┘└───────────┘└┘
249    -- remaining cases are easy
st   ──────────────────────────────
250    any_goals { intros, simp [h], done },
id                               
src    └──────────┘└────┘└┘└────┘ └┘└───┘
typ    └──────────┘└────┘└┘└────┘└┘└───┘
doc    └──────────┘└────┘└┘└────┘ └┘└───┘
txt    └──────────┘└────┘└┘└────┘ └┘└───┘
par    └──────────┘└────┘└┘└────┘ └┘└───┘
pid             └───────────────┘ └───────┘
st   ────────────┘└─────┘└────────┘└───────┘
251    all_goals { intros, simp [ih h], done },
id                               └┘ 
src    └──────────┘└────┘└┘└────┘   └┘└───┘
typ    └──────────┘└────┘└┘└────┘└┘└┘└───┘
doc    └──────────┘└────┘└┘└────┘   └┘└───┘
txt    └──────────┘└────┘└┘└────┘   └┘└───┘
par    └──────────┘└────┘└┘└────┘   └┘└───┘
pid             └───────────────┘   └───────┘
st   ────────────┘└─────┘└───────────┘└─────────
252  end
st   ──┘
253  
254  lemma mem_mk_insert_result {a t} (c) : mem lt a t → mem lt a (mk_insert_result c t) :=
id                                          └─┘ └┘     └─┘ └┘   └──────────────┘  
src                                         └─┘          └─┘       └──────────────┘
typ                                         └─┘ └┘     └─┘ └┘   └──────────────┘  
255  by intros; cases c; cases t; simp [mk_insert_result, mem, *] at *
id                                    └──────────────┘  └─┘
src     └────┘  └────┘   └────┘   └────┘└──────────────┘└┘└─┘└─────────
typ     └────┘  └────┘  └────┘  └────┘└──────────────┘└┘└─┘└─────────
doc     └────┘  └────┘   └────┘   └────┘                └┘   └─────────
txt     └────┘  └────┘   └────┘   └────┘                └┘   └─────────
par     └────┘  └────┘   └────┘   └────┘                └┘   └─────────
pid                                                 └┘   └──┘└──┘
st     └───────────────────────────────────────────────────────────────
256  
src  
typ  
doc  
txt  
par  
pid  
st   
257  lemma mem_of_mem_mk_insert_result {a t c} : mem lt a (mk_insert_result c t) → mem lt a t :=
id                                               └─┘ └┘   └──────────────┘      └─┘ └┘  
src                                              └─┘       └──────────────┘        └─┘
typ                                              └─┘ └┘   └──────────────┘      └─┘ └┘  
258  by cases t; cases c; simp [mk_insert_result, mem]; intros; assumption
id                            └──────────────┘  └─┘
src     └────┘   └────┘   └────┘└──────────────┘└┘└─┘  └────┘  └──────────
typ     └────┘  └────┘  └────┘└──────────────┘└┘└─┘  └────┘  └──────────
doc     └────┘   └────┘   └────┘                └┘     └────┘  └──────────
txt     └────┘   └────┘   └────┘                └┘     └────┘  └──────────
par     └────┘   └────┘   └────┘                └┘     └────┘  └──────────
pid                                         └┘                       
st     └───────────────────────────────────────────────────────────────────
259  
src  
typ  
doc  
txt  
par  
pid  
st   
260  lemma mem_insert_of_incomp (t : rbnode α) {x y : α} : ∀ h : ¬ lt x y ∧ ¬ lt y x, x ∈ t.insert lt y :=
id                                   └────┘                     └┘     └┘      └─────┘ └┘ 
src                                  └────┘                                            └─────┘
typ                                  └────┘                     └┘     └┘      └─────┘ └┘ 
261  by intros; unfold insert; apply mem_mk_insert_result; apply mem_ins_of_incomp; assumption
id                                   └──────────────────┘        └───────────────┘
src     └────┘  └───────────┘  └────┘└──────────────────┘  └────┘└───────────────┘  └──────────
typ     └────┘  └───────────┘  └────┘└──────────────────┘  └────┘└───────────────┘  └──────────
doc     └────┘  └───────────┘  └────┘                      └────┘                   └──────────
txt     └────┘  └───────────┘  └────┘                      └────┘                   └──────────
par     └────┘  └───────────┘  └────┘                      └────┘                   └──────────
pid                   └─────┘                                                               
st     └───────────────────────────────────────────────────────────────────────────────────────
262  
src  
typ  
doc  
txt  
par  
pid  
st   
263  lemma mem_insert_of_mem [is_strict_weak_order α lt] {t x} (z) : x ∈ t → x ∈ t.insert lt z :=
id                            └──────────────────┘  └┘                     └─────┘ └┘ 
src                           └──────────────────┘                              └─────┘
typ                           └──────────────────┘  └┘                     └─────┘ └┘ 
264  by intros; apply mem_mk_insert_result; apply mem_ins_of_mem; assumption
id                    └──────────────────┘        └────────────┘
src     └────┘  └────┘└──────────────────┘  └────┘└────────────┘  └──────────
typ     └────┘  └────┘└──────────────────┘  └────┘└────────────┘  └──────────
doc     └────┘  └────┘                      └────┘                └──────────
txt     └────┘  └────┘                      └────┘                └──────────
par     └────┘  └────┘                      └────┘                └──────────
pid                                                                       
st     └─────────────────────────────────────────────────────────────────────
265  
src  
typ  
doc  
txt  
par  
pid  
st   
266  lemma of_mem_balance1_node [is_strict_weak_order α lt] {x s v t} : x ∈ balance1_node s v t → x ∈ s ∨ (¬ lt x v ∧ ¬ lt v x) ∨ x ∈ t :=
id                               └──────────────────┘  └┘                └───────────┘            └┘     └┘       
src                              └──────────────────┘                      └───────────┘                                     
typ                              └──────────────────┘  └┘                └───────────┘            └┘     └┘       
267  begin
st   └─────
268    cases s; simp,
id           
src    └────┘   └──┘
typ    └────┘  └──┘
doc    └────┘   └──┘
txt    └────┘   └──┘
par    └────┘   └──┘
pid         
st   ──────────────┘└─
269    { intros, simp [*] },
src      └────┘  └───────┘
typ      └────┘  └───────┘
doc      └────┘  └───────┘
txt      └────┘  └───────┘
par      └────┘  └───────┘
pid                  └─┘
st   ───┘└────┘└─────────┘└┘
270    all_goals { apply balance.cases s_lchild s_val s_rchild; intros; simp [*] at *; blast_disjs; simp [*] }
id                       └───────────┘ └──────┘ └───┘ └──────┘
src    └──────────┘└────┘└───────────┘                     └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
typ    └──────────┘└────┘└───────────┘└──────┘└───┘└──────┘└┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
doc    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘           └┘└───────┘└┘
txt    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
par    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
pid             └───────┘                                  └──────────────────────────────────────────────┘
st   ────────────┘└─────────────────────────────────────────────────────────────────────────────────────────┘
271  end
st   └─┘
272  
273  lemma of_mem_balance2_node [is_strict_weak_order α lt] {x s v t} : x ∈ balance2_node s v t → x ∈ s ∨ (¬ lt x v ∧ ¬ lt v x) ∨ x ∈ t :=
id                               └──────────────────┘  └┘                └───────────┘            └┘     └┘       
src                              └──────────────────┘                      └───────────┘                                     
typ                              └──────────────────┘  └┘                └───────────┘            └┘     └┘       
274  begin
st   └─────
275    cases s; simp,
id           
src    └────┘   └──┘
typ    └────┘  └──┘
doc    └────┘   └──┘
txt    └────┘   └──┘
par    └────┘   └──┘
pid         
st   ──────────────┘└─
276    { intros, simp [*] },
src      └────┘  └───────┘
typ      └────┘  └───────┘
doc      └────┘  └───────┘
txt      └────┘  └───────┘
par      └────┘  └───────┘
pid                  └─┘
st   ───┘└────┘└─────────┘└┘
277    all_goals { apply balance.cases s_lchild s_val s_rchild; intros; simp [*] at *; blast_disjs; simp [*] }
id                       └───────────┘ └──────┘ └───┘ └──────┘
src    └──────────┘└────┘└───────────┘                     └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
typ    └──────────┘└────┘└───────────┘└──────┘└───┘└──────┘└┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
doc    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘           └┘└───────┘└┘
txt    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
par    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
pid             └───────┘                                  └──────────────────────────────────────────────┘
st   ────────────┘└─────────────────────────────────────────────────────────────────────────────────────────┘
278  end
st   └─┘
279  
280  lemma equiv_or_mem_of_mem_ins [is_strict_weak_order α lt] {t : rbnode α} {x z} : ∀ (h : x ∈ t.ins lt z), x ≈[lt] z ∨ x ∈ t :=
id                                  └──────────────────┘  └┘       └────┘                    └──┘ └┘     └┘└┘     
src                                 └──────────────────┘            └────┘                       └──┘          └┘        
typ                                 └──────────────────┘  └┘       └────┘                    └──┘ └┘     └┘└┘     
281  begin
st   └─────
282    with_cases { apply ins.induction lt t z; intros; simp [ins, strict_weak_order.equiv, *] at *; blast_disjs },
id                        └───────────┘ └┘                  └─┘  └─────────────────────┘
src    └───────────┘└────┘└───────────┘    └┘└────┘└┘└────┘└─┘└┘└─────────────────────┘└───────┘└┘└──────────┘
typ    └───────────┘└────┘└───────────┘└┘└┘└────┘└┘└────┘└─┘└┘└─────────────────────┘└───────┘└┘└──────────┘
doc    └───────────┘└────┘                 └┘└────┘└┘└────┘   └┘                       └───────┘└┘            
txt    └───────────┘└────┘                 └┘└────┘└┘└────┘   └┘                       └───────┘└┘└──────────┘
par    └───────────┘└────┘                 └┘└────┘└┘└────┘   └┘                       └───────┘└┘└──────────┘
pid              └───────┘                 └──────────────┘   └┘                       └──────────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────┘└┘
283    case is_black_lt_red {
src    └──────────────────────
typ    └──────────────────────
doc    └──────────────────────
txt    └──────────────────────
par    └──────────────────────
pid        └──────────────┘└─
st   ───────────────────────┘
284       have h' := of_mem_balance1_node lt h, blast_disjs,
id                   └──────────────────┘ └┘ 
src  ────┘└─────────┘└──────────────────┘   └┘└─────────┘└─
typ  ────┘└─────────┘└──────────────────┘└┘└┘└─────────┘└─
doc  ────┘└─────────┘                       └┘           └─
txt  ────┘└─────────┘                       └┘└─────────┘└─
par  ────┘└─────────┘                       └┘└─────────┘└─
pid  ───────────────┘                       └──────────────
st   ────────────────────────────────────────┘└───────────┘└─
285       have := ih h', blast_disjs,
id                └┘ └┘
src  ────┘└──────┘    └┘└─────────┘└─
typ  ────┘└──────┘└┘└┘└┘└─────────┘└─
doc  ────┘└──────┘    └┘           └─
txt  ────┘└──────┘    └┘└─────────┘└─
par  ────┘└──────┘    └┘└─────────┘└─
pid  ────────────┘    └──────────────
st   ─────────────────┘└───────────┘└─
286       all_goals { simp [h, *] } },
id                          
src  ────┘└──────────┘└────┘ └───┘└┘
typ  ────┘└──────────┘└────┘└───┘└┘
doc  ────┘└──────────┘└────┘ └───┘└┘
txt  ────┘└──────────┘└────┘ └───┘└┘
par  ────┘└──────────┘└────┘ └───┘└┘
pid  ──────────────────────┘ └──────┘
st   ───────────────┘└───────────┘└┘
287    case is_black_gt_red {
src    └──────────────────────
typ    └──────────────────────
doc    └──────────────────────
txt    └──────────────────────
par    └──────────────────────
pid        └──────────────┘└─
st   ───────────────────────┘
288       have h' := of_mem_balance2_node lt h, blast_disjs,
id                   └──────────────────┘ └┘ 
src  ────┘└─────────┘└──────────────────┘   └┘└─────────┘└─
typ  ────┘└─────────┘└──────────────────┘└┘└┘└─────────┘└─
doc  ────┘└─────────┘                       └┘           └─
txt  ────┘└─────────┘                       └┘└─────────┘└─
par  ────┘└─────────┘                       └┘└─────────┘└─
pid  ───────────────┘                       └──────────────
st   ────────────────────────────────────────┘└───────────┘└─
289       have := ih h', blast_disjs,
id                └┘ └┘
src  ────┘└──────┘    └┘└─────────┘└─
typ  ────┘└──────┘└┘└┘└┘└─────────┘└─
doc  ────┘└──────┘    └┘           └─
txt  ────┘└──────┘    └┘└─────────┘└─
par  ────┘└──────┘    └┘└─────────┘└─
pid  ────────────┘    └──────────────
st   ─────────────────┘└───────────┘└─
290       all_goals { simp [h, *] }},
id                          
src  ────┘└──────────┘└────┘ └───┘
typ  ────┘└──────────┘└────┘└───┘
doc  ────┘└──────────┘└────┘ └───┘
txt  ────┘└──────────┘└────┘ └───┘
par  ────┘└──────────┘└────┘ └───┘
pid  ──────────────────────┘ └─────┘
st   ───────────────┘└───────────┘└─┘
291    -- All other goals can be solved by the following tactics
st   ────────────────────────────────────────────────────────────
292    any_goals { intros, simp [h] },
id                               
src    └──────────┘└────┘└┘└────┘ └┘
typ    └──────────┘└────┘└┘└────┘└┘
doc    └──────────┘└────┘└┘└────┘ └┘
txt    └──────────┘└────┘└┘└────┘ └┘
par    └──────────┘└────┘└┘└────┘ └┘
pid             └───────────────┘ └─┘
st   ────────────┘└─────┘└─────────┘└┘
293    all_goals { intros, have ih := ih h, cases ih; simp [*], done },
id                                    └┘         └┘
src    └──────────┘└────┘└┘└─────────┘   └┘└────┘  └┘└──────┘└┘└───┘
typ    └──────────┘└────┘└┘└─────────┘└┘└┘└────┘└┘└┘└──────┘└┘└───┘
doc    └──────────┘└────┘└┘└─────────┘   └┘└────┘  └┘└──────┘└┘└───┘
txt    └──────────┘└────┘└┘└─────────┘   └┘└────┘  └┘└──────┘└┘└───┘
par    └──────────┘└────┘└┘└─────────┘   └┘└────┘  └┘└──────┘└┘└───┘
pid             └────────────────────┘   └──────┘  └────────────────┘
st   ────────────┘└─────┘└───────────────┘└──────────────────┘└─────────
294  end
st   ──┘
295  
296  lemma equiv_or_mem_of_mem_insert [is_strict_weak_order α lt] {t : rbnode α} {x z} : ∀ (h : x ∈ t.insert lt z), x ≈[lt] z ∨ x ∈ t :=
id                                     └──────────────────┘  └┘       └────┘                    └─────┘ └┘     └┘└┘     
src                                    └──────────────────┘            └────┘                       └─────┘          └┘        
typ                                    └──────────────────┘  └┘       └────┘                    └─────┘ └┘     └┘└┘     
297  begin
st   └─────
298    simp [insert], intros, apply equiv_or_mem_of_mem_ins, exact mem_of_mem_mk_insert_result lt h
id           └────┘                 └─────────────────────┘        └─────────────────────────┘ └┘ 
src    └────┘└────┘  └────┘  └────┘└─────────────────────┘  └────┘└─────────────────────────┘   
typ    └────┘└────┘  └────┘  └────┘└─────────────────────┘  └────┘└─────────────────────────┘└┘
doc    └────┘        └────┘  └────┘                         └────┘                              
txt    └────┘        └────┘  └────┘                         └────┘                              
par    └────┘        └────┘  └────┘                         └────┘                              
pid                                                                                         
st   ──────────────┘└──────┘└─────────────────────────────┘└───────────────────────────────────────┘
299  end
st   └─┘
300  
301  local attribute [simp] mem_exact
id                          └───────┘
src                         └───────┘
typ                         └───────┘
doc                   └──┘
302  
303  lemma mem_exact_balance1_node_of_mem_exact {x s} (v) (t : rbnode α) : mem_exact x s → mem_exact x (balance1_node s v t) :=
id                                                             └────┘     └───────┘     └───────┘   └───────────┘   
src                                                            └────┘      └───────┘       └───────┘    └───────────┘
typ                                                            └────┘     └───────┘     └───────┘   └───────────┘   
304  begin
st   └─────
305    cases s; simp,
id           
src    └────┘   └──┘
typ    └────┘  └──┘
doc    └────┘   └──┘
txt    └────┘   └──┘
par    └────┘   └──┘
pid         
st   ──────────────┘└─
306    all_goals { apply balance.cases s_lchild s_val s_rchild; intros; simp [*] at *; blast_disjs; simp [*] }
id                       └───────────┘ └──────┘ └───┘ └──────┘
src    └──────────┘└────┘└───────────┘                     └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
typ    └──────────┘└────┘└───────────┘└──────┘└───┘└──────┘└┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
doc    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘           └┘└───────┘└┘
txt    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
par    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
pid             └───────┘                                  └──────────────────────────────────────────────┘
st   ────────────┘└─────────────────────────────────────────────────────────────────────────────────────────┘
307  end
st   └─┘
308  
309  lemma mem_exact_balance2_node_of_mem_exact {x s} (v) (t : rbnode α) : mem_exact x s → mem_exact x (balance2_node s v t) :=
id                                                             └────┘     └───────┘     └───────┘   └───────────┘   
src                                                            └────┘      └───────┘       └───────┘    └───────────┘
typ                                                            └────┘     └───────┘     └───────┘   └───────────┘   
310  begin
st   └─────
311    cases s; simp,
id           
src    └────┘   └──┘
typ    └────┘  └──┘
doc    └────┘   └──┘
txt    └────┘   └──┘
par    └────┘   └──┘
pid         
st   ──────────────┘└─
312    all_goals { apply balance.cases s_lchild s_val s_rchild; intros; simp [*] at *; blast_disjs; simp [*] }
id                       └───────────┘ └──────┘ └───┘ └──────┘
src    └──────────┘└────┘└───────────┘                     └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
typ    └──────────┘└────┘└───────────┘└──────┘└───┘└──────┘└┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
doc    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘           └┘└───────┘└┘
txt    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
par    └──────────┘└────┘                                  └┘└────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘
pid             └───────┘                                  └──────────────────────────────────────────────┘
st   ────────────┘└─────────────────────────────────────────────────────────────────────────────────────────┘
313  end
st   └─┘
314  
315  lemma find_balance1_node [is_strict_weak_order α lt] {x y z t s} : ∀ {lo hi}, is_searchable lt t lo (some z) → is_searchable lt s (some z) hi → find lt t y = some x → y ≈[lt] x → find lt (balance1_node t z s) y = some x :=
id                             └──────────────────┘  └┘                   └┘ └┘   └───────────┘ └┘  └┘  └──┘     └───────────┘ └┘   └──┘   └┘   └──┘ └┘    └──┘     └┘└┘    └──┘ └┘  └───────────┘       └──┘ 
src                            └──────────────────┘                                └───────────┘          └──┘      └───────────┘       └──┘         └──┘         └──┘       └┘       └──┘     └───────────┘           └──┘
typ                            └──────────────────┘  └┘                   └┘ └┘   └───────────┘ └┘  └┘  └──┘     └───────────┘ └┘   └──┘   └┘   └──┘ └┘    └──┘     └┘└┘    └──┘ └┘  └───────────┘       └──┘ 
316  begin
st   └─────
317    intros _ _ hs₁ hs₂ heq heqv,
src    └─────────────────────────┘
typ    └─────────────────────────┘
doc    └─────────────────────────┘
txt    └─────────────────────────┘
par    └─────────────────────────┘
pid          └───────────────────┘
st   ────────────────────────────┘└─
318    have hs := is_searchable_balance1_node lt hs₁ hs₂,
id                └─────────────────────────┘ └┘ └─┘ └─┘
src    └─────────┘└─────────────────────────┘     
typ    └─────────┘└─────────────────────────┘└┘└─┘└─┘
doc    └─────────┘                                
txt    └─────────┘                                
par    └─────────┘                                
pid    └─────┘└─┘                                
st   ──────────────────────────────────────────────────┘└─
319    have := eq.trans (find_eq_find_of_eqv hs₁ heqv.symm) heq,
id             └──────┘  └─────────────────┘ └─┘ └───────┘  └─┘
src    └──────┘└──────┘ └─────────────────┘   └───────┘└┘└─┘
typ    └──────┘└──────┘ └─────────────────┘└─┘└───────┘└┘└─┘
doc    └──────┘                                        └┘
txt    └──────┘                                        └┘
par    └──────┘                                        └┘
pid    └───┘└─┘                                        └┘
st   ─────────────────────────────────────────────────────────┘└─
320    have := iff.mpr (find_correct_exact hs₁) this,
id             └─────┘  └────────────────┘ └─┘  └──┘
src    └──────┘└─────┘ └────────────────┘   └┘
typ    └──────┘└─────┘ └────────────────┘└─┘└┘└──┘
doc    └──────┘                             └┘
txt    └──────┘                             └┘
par    └──────┘                             └┘
pid    └───┘└─┘                             └┘
st   ──────────────────────────────────────────────┘└─
321    have := mem_exact_balance1_node_of_mem_exact z s this,
id             └──────────────────────────────────┘   └──┘
src    └──────┘└──────────────────────────────────┘  
typ    └──────┘└──────────────────────────────────┘└──┘
doc    └──────┘                                      
txt    └──────┘                                      
par    └──────┘                                      
pid    └───┘└─┘                                      
st   ──────────────────────────────────────────────────────┘└─
322    have := iff.mp (find_correct_exact hs) this,
id             └────┘  └────────────────┘ └┘  └──┘
src    └──────┘└────┘ └────────────────┘  └┘
typ    └──────┘└────┘ └────────────────┘└┘└┘└──┘
doc    └──────┘                           └┘
txt    └──────┘                           └┘
par    └──────┘                           └┘
pid    └───┘└─┘                           └┘
st   ────────────────────────────────────────────┘└─
323    exact eq.trans (find_eq_find_of_eqv hs heqv) this
id           └──────┘  └─────────────────┘ └┘ └──┘  └──┘
src    └────┘└──────┘ └─────────────────┘      └┘    
typ    └────┘└──────┘ └─────────────────┘└┘└──┘└┘└──┘
doc    └────┘                                  └┘    
txt    └────┘                                  └┘    
par    └────┘                                  └┘    
pid                                           └┘    
st   ───────────────────────────────────────────────────┘
324  end
st   └─┘
325  
326  lemma find_balance2_node [is_strict_weak_order α lt] {x y z s t} [is_trans α lt] : ∀ {lo hi}, is_searchable lt s lo (some z) → is_searchable lt t (some z) hi → find lt t y = some x → y ≈[lt] x → find lt (balance2_node t z s) y = some x :=
id                             └──────────────────┘  └┘               └──────┘  └┘       └┘ └┘   └───────────┘ └┘  └┘  └──┘     └───────────┘ └┘   └──┘   └┘   └──┘ └┘    └──┘     └┘└┘    └──┘ └┘  └───────────┘       └──┘ 
src                            └──────────────────┘                    └──────┘                    └───────────┘          └──┘      └───────────┘       └──┘         └──┘         └──┘       └┘       └──┘     └───────────┘           └──┘
typ                            └──────────────────┘  └┘               └──────┘  └┘       └┘ └┘   └───────────┘ └┘  └┘  └──┘     └───────────┘ └┘   └──┘   └┘   └──┘ └┘    └──┘     └┘└┘    └──┘ └┘  └───────────┘       └──┘ 
327  begin
st   └─────
328    intros _ _ hs₁ hs₂ heq heqv,
src    └─────────────────────────┘
typ    └─────────────────────────┘
doc    └─────────────────────────┘
txt    └─────────────────────────┘
par    └─────────────────────────┘
pid          └───────────────────┘
st   ────────────────────────────┘└─
329    have hs := is_searchable_balance2_node lt hs₁ hs₂,
id                └─────────────────────────┘ └┘ └─┘ └─┘
src    └─────────┘└─────────────────────────┘     
typ    └─────────┘└─────────────────────────┘└┘└─┘└─┘
doc    └─────────┘                                
txt    └─────────┘                                
par    └─────────┘                                
pid    └─────┘└─┘                                
st   ──────────────────────────────────────────────────┘└─
330    have := eq.trans (find_eq_find_of_eqv hs₂ heqv.symm) heq,
id             └──────┘  └─────────────────┘ └─┘ └───────┘  └─┘
src    └──────┘└──────┘ └─────────────────┘   └───────┘└┘└─┘
typ    └──────┘└──────┘ └─────────────────┘└─┘└───────┘└┘└─┘
doc    └──────┘                                        └┘
txt    └──────┘                                        └┘
par    └──────┘                                        └┘
pid    └───┘└─┘                                        └┘
st   ─────────────────────────────────────────────────────────┘└─
331    have := iff.mpr (find_correct_exact hs₂) this,
id             └─────┘  └────────────────┘ └─┘  └──┘
src    └──────┘└─────┘ └────────────────┘   └┘
typ    └──────┘└─────┘ └────────────────┘└─┘└┘└──┘
doc    └──────┘                             └┘
txt    └──────┘                             └┘
par    └──────┘                             └┘
pid    └───┘└─┘                             └┘
st   ──────────────────────────────────────────────┘└─
332    have := mem_exact_balance2_node_of_mem_exact z s this,
id             └──────────────────────────────────┘   └──┘
src    └──────┘└──────────────────────────────────┘  
typ    └──────┘└──────────────────────────────────┘└──┘
doc    └──────┘                                      
txt    └──────┘                                      
par    └──────┘                                      
pid    └───┘└─┘                                      
st   ──────────────────────────────────────────────────────┘└─
333    have := iff.mp (find_correct_exact hs) this,
id             └────┘  └────────────────┘ └┘  └──┘
src    └──────┘└────┘ └────────────────┘  └┘
typ    └──────┘└────┘ └────────────────┘└┘└┘└──┘
doc    └──────┘                           └┘
txt    └──────┘                           └┘
par    └──────┘                           └┘
pid    └───┘└─┘                           └┘
st   ────────────────────────────────────────────┘└─
334    exact eq.trans (find_eq_find_of_eqv hs heqv) this
id           └──────┘  └─────────────────┘ └┘ └──┘  └──┘
src    └────┘└──────┘ └─────────────────┘      └┘    
typ    └────┘└──────┘ └─────────────────┘└┘└──┘└┘└──┘
doc    └────┘                                  └┘    
txt    └────┘                                  └┘    
par    └────┘                                  └┘    
pid                                           └┘    
st   ───────────────────────────────────────────────────┘
335  end
st   └─┘
336  
337  /- Auxiliary lemma -/
338  
339  lemma ite_eq_of_not_lt [is_strict_order α lt] {a b} {β : Type v} (t s : β) (h : lt b a) : (if lt a b then t else s) = s :=
id                           └─────────────┘  └┘                                   └┘          └┘                 
src                          └─────────────┘                                                                             
typ                          └─────────────┘  └┘                                   └┘          └┘                 
340  begin have := not_lt_of_lt h, simp [*] end
id                 └──────────┘ 
src        └──────┘└──────────┘   └───────┘
typ        └──────┘└──────────┘  └───────┘
doc        └──────┘               └───────┘
txt        └──────┘               └───────┘
par        └──────┘               └───────┘
pid        └───┘└─┘                   └─┘
st   └──────────────────────────┘└─────────┘└─┘
341  
342  local attribute [simp] ite_eq_of_not_lt
id                          └──────────────┘
src                         └──────────────┘
typ                         └──────────────┘
doc                   └──┘
343  
344  private meta def simp_fi : tactic unit :=
id                              └────┘ └──┘
src                             └────┘ └──┘
typ                             └────┘ └──┘
doc                                    └──┘
345  `[simp [find, ins, *, cmp_using]]
src    └────┘    └┘   └───┘         
typ    └────┘    └┘   └───┘         
doc    └────┘    └┘   └───┘         
txt    └────┘    └┘   └───┘         
par    └────┘    └┘   └───┘         
pid            └┘   └───┘         
346  
347  lemma find_ins_of_eqv [is_strict_weak_order α lt] {x y : α} {t : rbnode α} (he : x ≈[lt] y) : ∀ {lo hi} (hs : is_searchable lt t lo hi) (hlt₁ : lift lt lo (some x)) (hlt₂ : lift lt (some x) hi), find lt (ins lt t x) y = some x :=
id                          └──────────────────┘  └┘                └────┘          └┘└┘        └┘ └┘        └───────────┘ └┘  └┘ └┘          └──┘ └┘ └┘  └──┘            └──┘ └┘  └──┘   └┘   └──┘ └┘  └─┘ └┘      └──┘ 
src                         └──────────────────┘                      └────┘            └┘                        └───────────┘                     └──┘        └──┘             └──┘     └──┘         └──┘     └─┘            └──┘
typ                         └──────────────────┘  └┘                └────┘          └┘└┘        └┘ └┘        └───────────┘ └┘  └┘ └┘          └──┘ └┘ └┘  └──┘            └──┘ └┘  └──┘   └┘   └──┘ └┘  └─┘ └┘      └──┘ 
348  begin
st   └─────
349    simp [strict_weak_order.equiv] at he,
id           └─────────────────────┘
src    └────┘└─────────────────────┘└─────┘
typ    └────┘└─────────────────────┘└─────┘
doc    └────┘                       └─────┘
txt    └────┘                       └─────┘
par    └────┘                       └─────┘
pid                               └───┘
st   ─────────────────────────────────────┘└─
350    apply ins.induction lt t x; intros,
id           └───────────┘ └┘  
src    └────┘└───────────┘      └────┘
typ    └────┘└───────────┘└┘  └────┘
doc    └────┘                   └────┘
txt    └────┘                   └────┘
par    └────┘                   └────┘
pid                         
st   ───────────────────────────────────┘└─
351    { simp_fi },
id       └─────┘
src      └─────┘
typ      └─────┘
par      └─────┘
st   ───┘└─────┘└─┘
352    all_goals { simp at hc, cases hs },
id                                   └┘
src    └──────────┘└────────┘└┘└────┘  
typ    └──────────┘└────────┘└┘└────┘└┘
doc    └──────────┘└────────┘└┘└────┘  
txt    └──────────┘└────────┘└┘└────┘  
par    └──────────┘└────────┘└┘└────┘  
pid             └───────────────────┘  └┘
st   ────────────┘└─────────┘└─────────┘└┘
353    { have := lt_of_incomp_of_lt he.swap hc,
id               └────────────────┘ └─────┘ └┘
src      └──────┘└────────────────┘└─────┘
typ      └──────┘└────────────────┘└─────┘└┘
doc      └──────┘                         
txt      └──────┘                         
par      └──────┘                         
pid      └───┘└─┘                         
st   ───┘└───────────────────────────────────┘└─
354      have := ih hs_hs₁ hlt₁ hc,
id               └┘ └────┘ └──┘ └┘
src      └──────┘            
typ      └──────┘└┘└────┘└──┘└┘
doc      └──────┘            
txt      └──────┘            
par      └──────┘            
pid      └───┘└─┘            
st   ────────────────────────────┘└─
355      simp_fi },
id       └─────┘
src      └─────┘
typ      └─────┘
par      └─────┘
st   ──────────┘└─┘
356    { simp_fi },
id       └─────┘
src      └─────┘
typ      └─────┘
par      └─────┘
st   ───┘└─────┘└─┘
357    { have := lt_of_lt_of_incomp hc he,
id               └────────────────┘ └┘ └┘
src      └──────┘└────────────────┘  
typ      └──────┘└────────────────┘└┘└┘
doc      └──────┘                    
txt      └──────┘                    
par      └──────┘                    
pid      └───┘└─┘                    
st   ───┘└──────────────────────────────┘└─
358      have := ih hs_hs₂ hc hlt₂,
id               └┘ └────┘ └┘ └──┘
src      └──────┘          
typ      └──────┘└┘└────┘└┘└──┘
doc      └──────┘          
txt      └──────┘          
par      └──────┘          
pid      └───┘└─┘          
st   ────────────────────────────┘└─
359      simp_fi },
id       └─────┘
src      └─────┘
typ      └─────┘
par      └─────┘
st   ──────────┘└─┘
360    { simp_fi,
id       └─────┘
src      └─────┘
typ      └─────┘
par      └─────┘
st   ───┘└─────┘└─
361      have := is_searchable_ins lt hs_hs₁ hlt₁ hc,
id               └───────────────┘ └┘ └────┘ └──┘ └┘
src      └──────┘└───────────────┘            
typ      └──────┘└───────────────┘└┘└────┘└──┘└┘
doc      └──────┘                             
txt      └──────┘                             
par      └──────┘                             
pid      └───┘└─┘                             
st   ──────────────────────────────────────────────┘└─
362      apply find_balance1_node lt this hs_hs₂ (ih hs_hs₁ hlt₁ hc) he.symm },
id             └────────────────┘ └┘ └──┘ └────┘  └┘ └────┘ └──┘ └┘  └─────┘
src      └────┘└────────────────┘                           └┘└─────┘
typ      └────┘└────────────────┘└┘└──┘└────┘ └┘└────┘└──┘└┘└┘└─────┘
doc      └────┘                                             └┘       
txt      └────┘                                             └┘       
par      └────┘                                             └┘       
pid                                                        └┘       
st   ───────────────────────────────────────────────────────────────────────┘└┘
363    { have := lt_of_incomp_of_lt he.swap hc,
id               └────────────────┘ └─────┘ └┘
src      └──────┘└────────────────┘└─────┘
typ      └──────┘└────────────────┘└─────┘└┘
doc      └──────┘                         
txt      └──────┘                         
par      └──────┘                         
pid      └───┘└─┘                         
st   ───┘└───────────────────────────────────┘└─
364      have := ih hs_hs₁ hlt₁ hc,
id               └┘ └────┘ └──┘ └┘
src      └──────┘            
typ      └──────┘└┘└────┘└──┘└┘
doc      └──────┘            
txt      └──────┘            
par      └──────┘            
pid      └───┘└─┘            
st   ────────────────────────────┘└─
365      simp_fi },
id       └─────┘
src      └─────┘
typ      └─────┘
par      └─────┘
st   ──────────┘└─┘
366    { simp_fi },
id       └─────┘
src      └─────┘
typ      └─────┘
par      └─────┘
st   ───┘└─────┘└─┘
367    { simp_fi,
id       └─────┘
src      └─────┘
typ      └─────┘
par      └─────┘
st   ───┘└─────┘└─
368      have := is_searchable_ins lt hs_hs₂ hc hlt₂,
id               └───────────────┘ └┘ └────┘ └┘ └──┘
src      └──────┘└───────────────┘          
typ      └──────┘└───────────────┘└┘└────┘└┘└──┘
doc      └──────┘                           
txt      └──────┘                           
par      └──────┘                           
pid      └───┘└─┘                           
st   ──────────────────────────────────────────────┘└─
369      apply find_balance2_node lt hs_hs₁ this (ih hs_hs₂ hc hlt₂) he.symm },
id             └────────────────┘ └┘ └────┘ └──┘  └┘ └────┘ └┘ └──┘  └─────┘
src      └────┘└────────────────┘                           └┘└─────┘
typ      └────┘└────────────────┘└┘└────┘└──┘ └┘└────┘└┘└──┘└┘└─────┘
doc      └────┘                                             └┘       
txt      └────┘                                             └┘       
par      └────┘                                             └┘       
pid                                                        └┘       
st   ───────────────────────────────────────────────────────────────────────┘└┘
370    { have := lt_of_lt_of_incomp hc he,
id               └────────────────┘ └┘ └┘
src      └──────┘└────────────────┘  
typ      └──────┘└────────────────┘└┘└┘
doc      └──────┘                    
txt      └──────┘                    
par      └──────┘                    
pid      └───┘└─┘                    
st   ───────────────────────────────────┘└─
371      have := ih hs_hs₂ hc hlt₂,
id               └┘ └────┘ └┘ └──┘
src      └──────┘          
typ      └──────┘└┘└────┘└┘└──┘
doc      └──────┘          
txt      └──────┘          
par      └──────┘          
pid      └───┘└─┘          
st   ────────────────────────────┘└─
372      simp_fi }
id       └─────┘
src      └─────┘
typ      └─────┘
par      └─────┘
st   ──────────┘└──
373  end
st   ──┘
374  
375  lemma find_mk_insert_result (c : color) (t : rbnode α) (x : α) : find lt (mk_insert_result c t) x = find lt t x :=
id                                    └───┘       └────┘            └──┘ └┘  └──────────────┘      └──┘ └┘  
src                                   └───┘       └────┘              └──┘     └──────────────┘         └──┘
typ                                   └───┘       └────┘            └──┘ └┘  └──────────────┘      └──┘ └┘  
376  begin
st   └─────
377    cases t; cases c; simp [mk_insert_result],
id                           └──────────────┘
src    └────┘   └────┘   └────┘└──────────────┘
typ    └────┘  └────┘  └────┘└──────────────┘
doc    └────┘   └────┘   └────┘                
txt    └────┘   └────┘   └────┘                
par    └────┘   └────┘   └────┘                
pid                                        
st   ──────────────────────────────────────────┘└─
378    { simp [find], cases cmp_using lt x t_val; simp [find] }
id             └──┘         └───────┘ └┘  └───┘        └──┘
src      └────┘└──┘  └────┘└───────┘          └────┘└──┘└┘
typ      └────┘└──┘  └────┘└───────┘└┘└───┘  └────┘└──┘└┘
doc      └────┘      └────┘                   └────┘    └┘
txt      └────┘      └────┘                   └────┘    └┘
par      └────┘      └────┘                   └────┘    └┘
pid                                                
st   ──────────────┘└────────────────────────────────────────┘└─
379  end
st   ──┘
380  
381  lemma find_insert_of_eqv [is_strict_weak_order α lt] {x y : α} {t : rbnode α} (he : x ≈[lt] y) : is_searchable lt t none none → find lt (insert lt t x) y = some x :=
id                             └──────────────────┘  └┘                └────┘          └┘└┘     └───────────┘ └┘  └──┘ └──┘   └──┘ └┘  └────┘ └┘      └──┘ 
src                            └──────────────────┘                      └────┘            └┘        └───────────┘      └──┘ └──┘   └──┘     └────┘            └──┘
typ                            └──────────────────┘  └┘                └────┘          └┘└┘     └───────────┘ └┘  └──┘ └──┘   └──┘ └┘  └────┘ └┘      └──┘ 
382  begin
st   └─────
383    intro hs,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid         └─┘
st   ─────────┘└─
384    simp [insert, find_mk_insert_result],
id           └────┘  └───────────────────┘
src    └────┘└────┘└┘└───────────────────┘
typ    └────┘└────┘└┘└───────────────────┘
doc    └────┘      └┘                     
txt    └────┘      └┘                     
par    └────┘      └┘                     
pid              └┘                     
st   ─────────────────────────────────────┘└─
385    apply find_ins_of_eqv lt he hs; simp
id           └─────────────┘ └┘ └┘ └┘
src    └────┘└─────────────┘        └───┘
typ    └────┘└─────────────┘└┘└┘└┘  └───┘
doc    └────┘                       └───┘
txt    └────┘                       └───┘
par    └────┘                       └───┘
pid                                    
st   ──────────────────────────────────────┘
386  end
st   └─┘
387  
388  lemma weak_trichotomous (x y) {p : Prop} (is_lt : ∀ h : lt x y, p) (is_eqv : ∀ h : ¬ lt x y ∧ ¬ lt y x, p) (is_gt : ∀ h : lt y x, p) : p :=
id                                                           └┘                       └┘     └┘                     └┘        
src                                                                                              
typ                                                          └┘                       └┘     └┘                     └┘        
389  begin
st   └─────
390    by_cases lt x y; by_cases lt y x,
id              └┘             └┘  
src    └───────┘      └───────┘   
typ    └───────┘└┘  └───────┘└┘
doc    └───────┘      └───────┘   
txt    └───────┘      └───────┘   
par    └───────┘      └───────┘   
pid                             
st   ─────────────────────────────────┘└─
391    any_goals { apply is_lt; assumption },
src    └──────────┘└────┘     └┘└─────────┘
typ    └──────────┘└────┘     └┘└─────────┘
doc    └──────────┘└────┘     └┘└─────────┘
txt    └──────────┘└────┘     └┘└─────────┘
par    └──────────┘└────┘     └┘└─────────┘
pid             └───────┘     └────────────┘
st   ────────────┘└───────────────────────┘└┘
392    any_goals { apply is_gt; assumption },
src    └──────────┘└────┘     └┘└─────────┘
typ    └──────────┘└────┘     └┘└─────────┘
doc    └──────────┘└────┘     └┘└─────────┘
txt    └──────────┘└────┘     └┘└─────────┘
par    └──────────┘└────┘     └┘└─────────┘
pid             └───────┘     └────────────┘
st   ────────────┘└───────────────────────┘└┘
393    any_goals { apply is_eqv, constructor; assumption }
src    └──────────┘└────┘      └┘└─────────┘└┘└─────────┘└┘
typ    └──────────┘└────┘      └┘└─────────┘└┘└─────────┘└┘
doc    └──────────┘└────┘      └┘└─────────┘└┘└─────────┘└┘
txt    └──────────┘└────┘      └┘└─────────┘└┘└─────────┘└┘
par    └──────────┘└────┘      └┘└─────────┘└┘└─────────┘└┘
pid             └───────┘      └─────────────────────────┘
st   ─────────────────────────┘└────────────────────────┘
394  end
st   └─┘
395  
396  section find_ins_of_not_eqv
397  
398  section simp_aux_lemmas
399  
400  lemma find_black_eq_find_red {l y r x} : find lt (black_node l y r) x = find lt (red_node l y r) x :=
id                                            └──┘ └┘  └────────┘       └──┘ └┘  └──────┘     
src                                           └──┘     └────────┘           └──┘     └──────┘
typ                                           └──┘ └┘  └────────┘       └──┘ └┘  └──────┘     
401  begin simp [find], all_goals { cases cmp_using lt x y; simp [find] } end
id               └──┘                     └───────┘ └┘          └──┘
src        └────┘└──┘  └──────────┘└────┘└───────┘    └┘└────┘└──┘└┘└┘
typ        └────┘└──┘  └──────────┘└────┘└───────┘└┘└┘└────┘└──┘└┘└┘
doc        └────┘      └──────────┘└────┘             └┘└────┘    └┘└┘
txt        └────┘      └──────────┘└────┘             └┘└────┘    └┘└┘
par        └────┘      └──────────┘└────┘             └┘└────┘    └┘└┘
pid                           └───────┘             └──────┘    └─┘
st   └───────────────┘└────────────────────────────────────────────────┘└─┘
402  
403  lemma find_red_of_lt {l y r x} (h : lt x y) : find lt (red_node l y r) x = find lt l x :=
id                                       └┘      └──┘ └┘  └──────┘       └──┘ └┘  
src                                                └──┘     └──────┘           └──┘
typ                                      └┘      └──┘ └┘  └──────┘       └──┘ └┘  
404  by simp [find, cmp_using, *]
id            └──┘  └───────┘
src     └────┘└──┘└┘└───────┘└────
typ     └────┘└──┘└┘└───────┘└────
doc     └────┘    └┘         └────
txt     └────┘    └┘         └────
par     └────┘    └┘         └────
pid             └┘         └──┘
st     └──────────────────────────
405  
src  
typ  
doc  
txt  
par  
pid  
st   
406  lemma find_red_of_gt [is_strict_order α lt] {l y r x} (h : lt y x) : find lt (red_node l y r) x = find lt r x :=
id                         └─────────────┘  └┘                 └┘      └──┘ └┘  └──────┘       └──┘ └┘  
src                        └─────────────┘                                └──┘     └──────┘           └──┘
typ                        └─────────────┘  └┘                 └┘      └──┘ └┘  └──────┘       └──┘ └┘  
407  begin have := not_lt_of_lt h, simp [find, cmp_using, *]  end
id                 └──────────┘         └──┘  └───────┘
src        └──────┘└──────────┘   └────┘└──┘└┘└───────┘└────┘
typ        └──────┘└──────────┘  └────┘└──┘└┘└───────┘└────┘
doc        └──────┘               └────┘    └┘         └────┘
txt        └──────┘               └────┘    └┘         └────┘
par        └──────┘               └────┘    └┘         └────┘
pid        └───┘└─┘                       └┘         └──┘└┘
st   └──────────────────────────┘└───────────────────────────┘└─┘
408  
409  lemma find_red_of_incomp {l y r x} (h : ¬ lt x y ∧ ¬ lt y x) : find lt (red_node l y r) x = some y :=
id                                            └┘     └┘      └──┘ └┘  └──────┘       └──┘ 
src                                                              └──┘     └──────┘           └──┘
typ                                           └┘     └┘      └──┘ └┘  └──────┘       └──┘ 
410  by simp [find, cmp_using, *]
id            └──┘  └───────┘
src     └────┘└──┘└┘└───────┘└────
typ     └────┘└──┘└┘└───────┘└────
doc     └────┘    └┘         └────
txt     └────┘    └┘         └────
par     └────┘    └┘         └────
pid             └┘         └──┘
st     └──────────────────────────
411  
src  
typ  
doc  
txt  
par  
pid  
st   
412  end simp_aux_lemmas
413  
414  local attribute [simp]
doc                   └──┘
415    find_black_eq_find_red find_red_of_lt find_red_of_lt find_red_of_gt
id     └────────────────────┘ └────────────┘ └────────────┘ └────────────┘
src    └────────────────────┘ └────────────┘ └────────────┘ └────────────┘
typ    └────────────────────┘ └────────────┘ └────────────┘ └────────────┘
416    find_red_of_incomp
id     └────────────────┘
src    └────────────────┘
typ    └────────────────┘
417  
418  variable [is_strict_weak_order α lt]
id             └──────────────────┘
src            └──────────────────┘
typ            └──────────────────┘
419  
420  lemma find_balance1_lt {l r t v x y lo hi}
421                         (h : lt x y)
id                               └┘  
typ                              └┘  
422                         (hl : is_searchable lt l lo (some v))
id                                └───────────┘ └┘  └┘  └──┘ 
src                               └───────────┘          └──┘
typ                               └───────────┘ └┘  └┘  └──┘ 
423                         (hr : is_searchable lt r (some v) (some y))
id                                └───────────┘ └┘   └──┘    └──┘ 
src                               └───────────┘       └──┘     └──┘
typ                               └───────────┘ └┘   └──┘    └──┘ 
424                         (ht : is_searchable lt t (some y) hi)
id                                └───────────┘ └┘   └──┘   └┘
src                               └───────────┘       └──┘
typ                               └───────────┘ └┘   └──┘   └┘
425                         : find lt (balance1 l v r y t) x = find lt (red_node l v r) x :=
id                            └──┘ └┘  └──────┘         └──┘ └┘  └──────┘     
src                           └──┘     └──────┘               └──┘     └──────┘
typ                           └──┘ └┘  └──────┘         └──┘ └┘  └──────┘     
426  begin
st   └─────
427    with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
id                                         └───────────┘                       └──────────────────┘
src    └───────────┘└─────────────┘└┘└────┘└───────────┘   └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
typ    └───────────┘└─────────────┘└┘└────┘└───────────┘└┘└────┘└┘└──────┘└┘└──────────────────┘└┘
doc    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
txt    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
par    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
pid              └────────────────────────┘                └──────────────────┘                    └┘
st   ─────────────────────────────┘└─────────────────────────────────────────────────────────────────┘└─┘
428    case red_left : _ _ _ z r { apply weak_trichotomous lt z x; intros; simp [*] },
id                                       └───────────────┘ └┘  
src    └──────────────────────────┘└────┘└───────────────┘    └┘└────┘└┘└───────┘
typ    └──────────────────────────┘└────┘└───────────────┘└┘└┘└────┘└┘└───────┘
doc    └──────────────────────────┘└────┘                     └┘└────┘└┘└───────┘
txt    └──────────────────────────┘└────┘                     └┘└────┘└┘└───────┘
par    └──────────────────────────┘└────┘                     └┘└────┘└┘└───────┘
pid        └───────┘└──────────┘└───────┘                     └──────────────────┘
st   ────────────────────────────┘└────────────────────────────────────────────────┘└┘
429    case red_right : l_left l_val l_right z r {
src    └───────────────────────────────────────────
typ    └───────────────────────────────────────────
doc    └───────────────────────────────────────────
txt    └───────────────────────────────────────────
par    └───────────────────────────────────────────
pid        └────────┘└─────────────────────────┘└──
st   ────────────────────────────────────────────┘
430      with_cases { apply weak_trichotomous lt z x; intro h' },
id                          └───────────────┘ └┘  
src  ───┘└───────────┘└────┘└───────────────┘    └┘└───────┘└─
typ  ───┘└───────────┘└────┘└───────────────┘└┘└┘└───────┘└─
doc  ───┘└───────────┘└────┘                     └┘└───────┘└─
txt  ───┘└───────────┘└────┘                     └┘└───────┘└─
par  ───┘└───────────┘└────┘                     └┘└───────┘└─
pid  ──────────────────────┘                     └─────────────
st   ─────────────────────────────────────────────────────────┘└─
431      case is_lt  { have := trans_of lt (lo_lt_hi hr_hs₁) h', simp [*] },
id                             └──────┘ └┘  └──────┘ └────┘  └┘
src  ─────────────────┘└──────┘└──────┘   └──────┘      └┘  └┘└───────┘└──
typ  ─────────────────┘└──────┘└──────┘└┘ └──────┘└────┘└┘└┘└┘└───────┘└──
doc  ─────────────────┘└──────┘                         └┘  └┘└───────┘└──
txt  ─────────────────┘└──────┘                         └┘  └┘└───────┘└──
par  ─────────────────┘└──────┘                         └┘  └┘└───────┘└──
pid  ─────────────────────────┘                         └┘  └─────────────
st   ────────────────┘└───────────────────────────────────────┘└─────────┘└─
432      case is_eqv { have : lt l_val x := lt_of_lt_of_incomp (lo_lt_hi hr_hs₁) h', simp [*] },
id                            └┘ └───┘     └────────────────┘  └──────┘ └────┘  └┘
src  ─────────────────┘└─────┘        └──┘└────────────────┘ └──────┘      └┘  └┘└───────┘└──
typ  ─────────────────┘└─────┘└┘└───┘└──┘└────────────────┘ └──────┘└────┘└┘└┘└┘└───────┘└──
doc  ─────────────────┘└─────┘        └──┘                                 └┘  └┘└───────┘└──
txt  ─────────────────┘└─────┘        └──┘                                 └┘  └┘└───────┘└──
par  ─────────────────┘└─────┘        └──┘                                 └┘  └┘└───────┘└──
pid  ────────────────────────┘        └──┘                                 └┘  └─────────────
st   ────────────────┘└───────────────────────────────────────────────────────────┘└─────────┘└─
433      case is_gt  { apply weak_trichotomous lt l_val x; intros; simp [*] } }
id                           └───────────────┘ └┘ └───┘ 
src  ─────────────────┘└────┘└───────────────┘        └┘└────┘└┘└───────┘└──┘
typ  ─────────────────┘└────┘└───────────────┘└┘└───┘└┘└────┘└┘└───────┘└──┘
doc  ─────────────────┘└────┘                         └┘└────┘└┘└───────┘└──┘
txt  ─────────────────┘└────┘                         └┘└────┘└┘└───────┘└──┘
par  ─────────────────┘└────┘                         └┘└────┘└┘└───────┘└──┘
pid  ───────────────────────┘                         └────────────────────┘
st   ────────────────┘└────────────────────────────────────────────────────┘
434  end
st   └─┘
435  
436  meta def ins_ne_leaf_tac := `[apply ins_ne_leaf]
id            └─────────────┘
src                                └────┘
typ           └─────────────┘      └────┘
doc                                └────┘
txt                                └────┘
par                                └────┘
pid                                     
437  
438  lemma find_balance1_node_lt {t s x y lo hi} (hlt : lt y x)
id                                                      └┘  
typ                                                     └┘  
439                              (ht : is_searchable lt t lo (some x))
id                                     └───────────┘ └┘  └┘  └──┘ 
src                                    └───────────┘          └──┘
typ                                    └───────────┘ └┘  └┘  └──┘ 
440                              (hs : is_searchable lt s (some x) hi)
id                                     └───────────┘ └┘   └──┘   └┘
src                                    └───────────┘       └──┘
typ                                    └───────────┘ └┘   └──┘   └┘
441                              (hne : t ≠ leaf . ins_ne_leaf_tac)
id                                        └──┘ 
src                                        └──┘ 
typ                                       └──┘ 
doc                                       
442                              : find lt (balance1_node t x s) y = find lt t y :=
id                                 └──┘ └┘  └───────────┘       └──┘ └┘  
src                                └──┘     └───────────┘           └──┘
typ                                └──┘ └┘  └───────────┘       └──┘ └┘  
443  begin
st   └─────
444    cases t; simp [balance1_node],
id                   └───────────┘
src    └────┘   └────┘└───────────┘
typ    └────┘  └────┘└───────────┘
doc    └────┘   └────┘             
txt    └────┘   └────┘             
par    └────┘   └────┘             
pid                             
st   ──────────────────────────────┘└─
445    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
446    all_goals { intros, is_searchable_tactic, apply find_balance1_lt, assumption' }
id                         └──────────────────┘        └──────────────┘
src    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└──────────────┘└┘└──────────┘└┘
typ    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└──────────────┘└┘└──────────┘└┘
doc    └──────────┘└────┘└┘                    └┘└────┘                └┘└──────────┘└┘
txt    └──────────┘└────┘└┘                    └┘└────┘                └┘└──────────┘└┘
par    └──────────┘└────┘└┘└──────────────────┘└┘└────┘                └┘└──────────┘└┘
pid             └─────────┘                    └──────┘                └─────────────┘
st   ────────────┘└───────────────────────────┘└──────────────────────┘└────────────┘
447  end
st   └─┘
448  
449  lemma find_balance1_gt {l r t v x y lo hi}
450                         (h : lt y x)
id                               └┘  
typ                              └┘  
451                         (hl : is_searchable lt l lo (some v))
id                                └───────────┘ └┘  └┘  └──┘ 
src                               └───────────┘          └──┘
typ                               └───────────┘ └┘  └┘  └──┘ 
452                         (hr : is_searchable lt r (some v) (some y))
id                                └───────────┘ └┘   └──┘    └──┘ 
src                               └───────────┘       └──┘     └──┘
typ                               └───────────┘ └┘   └──┘    └──┘ 
453                         (ht : is_searchable lt t (some y) hi)
id                                └───────────┘ └┘   └──┘   └┘
src                               └───────────┘       └──┘
typ                               └───────────┘ └┘   └──┘   └┘
454                         : find lt (balance1 l v r y t) x = find lt t x :=
id                            └──┘ └┘  └──────┘         └──┘ └┘  
src                           └──┘     └──────┘               └──┘
typ                           └──┘ └┘  └──────┘         └──┘ └┘  
455  begin
st   └─────
456    with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
id                                         └───────────┘                       └──────────────────┘
src    └───────────┘└─────────────┘└┘└────┘└───────────┘   └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
typ    └───────────┘└─────────────┘└┘└────┘└───────────┘└┘└────┘└┘└──────┘└┘└──────────────────┘└┘
doc    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
txt    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
par    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
pid              └────────────────────────┘                └──────────────────┘                    └┘
st   ─────────────────────────────┘└─────────────────────────────────────────────────────────────────┘└─┘
457    case red_left : _ _ _ z {
src    └─────────────────────────
typ    └─────────────────────────
doc    └─────────────────────────
txt    └─────────────────────────
par    └─────────────────────────
pid        └───────┘└────────┘└──
st   ──────────────────────────┘
458      have := trans_of lt (lo_lt_hi hr) h, simp [*] },
id               └──────┘ └┘  └──────┘ └┘  
src  ───┘└──────┘└──────┘   └──────┘  └┘ └┘└───────┘
typ  ───┘└──────┘└──────┘└┘ └──────┘└┘└┘└┘└───────┘
doc  ───┘└──────┘                     └┘ └┘└───────┘
txt  ───┘└──────┘                     └┘ └┘└───────┘
par  ───┘└──────┘                     └┘ └┘└───────┘
pid  ───────────┘                     └┘ └──────────┘
st   ──────────────────────────────────────┘└─────────┘└┘
459    case red_right : _ _ _ z {
src    └──────────────────────────
typ    └──────────────────────────
doc    └──────────────────────────
txt    └──────────────────────────
par    └──────────────────────────
pid        └────────┘└────────┘└──
st   ───────────────────────────┘
460      have := trans_of lt (lo_lt_hi hr_hs₂) h, simp [*] }
id               └──────┘ └┘  └──────┘ └────┘  
src  ───┘└──────┘└──────┘   └──────┘      └┘ └┘└───────┘└┘
typ  ───┘└──────┘└──────┘└┘ └──────┘└────┘└┘└┘└───────┘└┘
doc  ───┘└──────┘                         └┘ └┘└───────┘└┘
txt  ───┘└──────┘                         └┘ └┘└───────┘└┘
par  ───┘└──────┘                         └┘ └┘└───────┘└┘
pid  ───────────┘                         └┘ └──────────┘
st   ──────────────────────────────────────────┘└─────────┘
461  end
st   └─┘
462  
463  lemma find_balance1_node_gt {t s x y lo hi} (h : lt x y)
id                                                    └┘  
typ                                                   └┘  
464                              (ht : is_searchable lt t lo (some x))
id                                     └───────────┘ └┘  └┘  └──┘ 
src                                    └───────────┘          └──┘
typ                                    └───────────┘ └┘  └┘  └──┘ 
465                              (hs : is_searchable lt s (some x) hi)
id                                     └───────────┘ └┘   └──┘   └┘
src                                    └───────────┘       └──┘
typ                                    └───────────┘ └┘   └──┘   └┘
466                              (hne : t ≠ leaf . ins_ne_leaf_tac)
id                                        └──┘ 
src                                        └──┘ 
typ                                       └──┘ 
doc                                       
467                              : find lt (balance1_node t x s) y = find lt s y :=
id                                 └──┘ └┘  └───────────┘       └──┘ └┘  
src                                └──┘     └───────────┘           └──┘
typ                                └──┘ └┘  └───────────┘       └──┘ └┘  
468  begin
st   └─────
469    cases t; simp [balance1_node],
id                   └───────────┘
src    └────┘   └────┘└───────────┘
typ    └────┘  └────┘└───────────┘
doc    └────┘   └────┘             
txt    └────┘   └────┘             
par    └────┘   └────┘             
pid                             
st   ──────────────────────────────┘└─
470    all_goals { intros, is_searchable_tactic, apply find_balance1_gt, assumption' }
id                         └──────────────────┘        └──────────────┘
src    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└──────────────┘└┘└──────────┘└┘
typ    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└──────────────┘└┘└──────────┘└┘
doc    └──────────┘└────┘└┘                    └┘└────┘                └┘└──────────┘└┘
txt    └──────────┘└────┘└┘                    └┘└────┘                └┘└──────────┘└┘
par    └──────────┘└────┘└┘└──────────────────┘└┘└────┘                └┘└──────────┘└┘
pid             └─────────┘                    └──────┘                └─────────────┘
st   ────────────┘└───────────────────────────┘└──────────────────────┘└────────────┘
471  end
st   └─┘
472  
473  lemma find_balance1_eqv {l r t v x y lo hi}
474                          (h : ¬ lt x y ∧ ¬ lt y x)
id                                 └┘     └┘  
src                                        
typ                                └┘     └┘  
475                          (hl : is_searchable lt l lo (some v))
id                                 └───────────┘ └┘  └┘  └──┘ 
src                                └───────────┘          └──┘
typ                                └───────────┘ └┘  └┘  └──┘ 
476                          (hr : is_searchable lt r (some v) (some y))
id                                 └───────────┘ └┘   └──┘    └──┘ 
src                                └───────────┘       └──┘     └──┘
typ                                └───────────┘ └┘   └──┘    └──┘ 
477                          (ht : is_searchable lt t (some y) hi)
id                                 └───────────┘ └┘   └──┘   └┘
src                                └───────────┘       └──┘
typ                                └───────────┘ └┘   └──┘   └┘
478                          : find lt (balance1 l v r y t) x = some y :=
id                             └──┘ └┘  └──────┘         └──┘ 
src                            └──┘     └──────┘               └──┘
typ                            └──┘ └┘  └──────┘         └──┘ 
479  begin
st   └─────
480    with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
id                                         └───────────┘                       └──────────────────┘
src    └───────────┘└─────────────┘└┘└────┘└───────────┘   └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
typ    └───────────┘└─────────────┘└┘└────┘└───────────┘└┘└────┘└┘└──────┘└┘└──────────────────┘└┘
doc    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
txt    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
par    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
pid              └────────────────────────┘                └──────────────────┘                    └┘
st   ─────────────────────────────┘└─────────────────────────────────────────────────────────────────┘└─┘
481    case red_left : _ _ _ z {
src    └─────────────────────────
typ    └─────────────────────────
doc    └─────────────────────────
txt    └─────────────────────────
par    └─────────────────────────
pid        └───────┘└────────┘└──
st   ──────────────────────────┘
482      have : lt z x := lt_of_lt_of_incomp (lo_lt_hi hr) h.swap,
id              └┘      └────────────────┘  └──────┘ └┘  └────┘
src  ───┘└─────┘    └──┘└────────────────┘ └──────┘  └┘└────┘└─
typ  ───┘└─────┘└┘└──┘└────────────────┘ └──────┘└┘└┘└────┘└─
doc  ───┘└─────┘    └──┘                             └┘      └─
txt  ───┘└─────┘    └──┘                             └┘      └─
par  ───┘└─────┘    └──┘                             └┘      └─
pid  ──────────┘    └──┘                             └┘      └─
st   ───────────────────────────────────────────────────────────┘└─
483      simp [*] },
src  ───┘└───────┘
typ  ───┘└───────┘
doc  ───┘└───────┘
txt  ───┘└───────┘
par  ───┘└───────┘
pid  ─────────────┘
st   ────────────┘└┘
484    case red_right : _ _ _ z {
src    └──────────────────────────
typ    └──────────────────────────
doc    └──────────────────────────
txt    └──────────────────────────
par    └──────────────────────────
pid        └────────┘└────────┘└──
st   ───────────────────────────┘
485      have : lt z x := lt_of_lt_of_incomp (lo_lt_hi hr_hs₂) h.swap,
id              └┘      └────────────────┘  └──────┘ └────┘  └────┘
src  ───┘└─────┘    └──┘└────────────────┘ └──────┘      └┘└────┘└─
typ  ───┘└─────┘└┘└──┘└────────────────┘ └──────┘└────┘└┘└────┘└─
doc  ───┘└─────┘    └──┘                                 └┘      └─
txt  ───┘└─────┘    └──┘                                 └┘      └─
par  ───┘└─────┘    └──┘                                 └┘      └─
pid  ──────────┘    └──┘                                 └┘      └─
st   ───────────────────────────────────────────────────────────────┘└─
486      simp [*] }
src  ───┘└───────┘└┘
typ  ───┘└───────┘└┘
doc  ───┘└───────┘└┘
txt  ───┘└───────┘└┘
par  ───┘└───────┘└┘
pid  ─────────────┘
st   ────────────┘
487  end
st   └─┘
488  
489  lemma find_balance1_node_eqv {t s x y lo hi}
490                               (h : ¬ lt x y ∧ ¬ lt y x)
id                                      └┘     └┘  
src                                             
typ                                     └┘     └┘  
491                               (ht : is_searchable lt t lo (some y))
id                                      └───────────┘ └┘  └┘  └──┘ 
src                                     └───────────┘          └──┘
typ                                     └───────────┘ └┘  └┘  └──┘ 
492                               (hs : is_searchable lt s (some y) hi)
id                                      └───────────┘ └┘   └──┘   └┘
src                                     └───────────┘       └──┘
typ                                     └───────────┘ └┘   └──┘   └┘
493                               (hne : t ≠ leaf . ins_ne_leaf_tac)
id                                         └──┘ 
src                                         └──┘ 
typ                                        └──┘ 
doc                                        
494                               : find lt (balance1_node t y s) x = some y :=
id                                  └──┘ └┘  └───────────┘       └──┘ 
src                                 └──┘     └───────────┘           └──┘
typ                                 └──┘ └┘  └───────────┘       └──┘ 
495  begin
st   └─────
496    cases t; simp [balance1_node],
id                   └───────────┘
src    └────┘   └────┘└───────────┘
typ    └────┘  └────┘└───────────┘
doc    └────┘   └────┘             
txt    └────┘   └────┘             
par    └────┘   └────┘             
pid                             
st   ──────────────────────────────┘└─
497    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
498    all_goals { intros, is_searchable_tactic, apply find_balance1_eqv, assumption' }
id                         └──────────────────┘        └───────────────┘
src    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└───────────────┘└┘└──────────┘└┘
typ    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└───────────────┘└┘└──────────┘└┘
doc    └──────────┘└────┘└┘                    └┘└────┘                 └┘└──────────┘└┘
txt    └──────────┘└────┘└┘                    └┘└────┘                 └┘└──────────┘└┘
par    └──────────┘└────┘└┘└──────────────────┘└┘└────┘                 └┘└──────────┘└┘
pid             └─────────┘                    └──────┘                 └─────────────┘
st   ────────────┘└───────────────────────────┘└───────────────────────┘└────────────┘
499  end
st   └─┘
500  
501  lemma find_balance2_lt {l v r t x y lo hi}
502                         (h :  lt x y)
id                                └┘  
typ                               └┘  
503                         (hl : is_searchable lt l (some y) (some v))
id                                └───────────┘ └┘   └──┘    └──┘ 
src                               └───────────┘       └──┘     └──┘
typ                               └───────────┘ └┘   └──┘    └──┘ 
504                         (hr : is_searchable lt r (some v) hi)
id                                └───────────┘ └┘   └──┘   └┘
src                               └───────────┘       └──┘
typ                               └───────────┘ └┘   └──┘   └┘
505                         (ht : is_searchable lt t lo (some y))
id                                └───────────┘ └┘  └┘  └──┘ 
src                               └───────────┘          └──┘
typ                               └───────────┘ └┘  └┘  └──┘ 
506                         : find lt (balance2 l v r y t) x = find lt t x :=
id                            └──┘ └┘  └──────┘         └──┘ └┘  
src                           └──┘     └──────┘               └──┘
typ                           └──┘ └┘  └──────┘         └──┘ └┘  
507  begin
st   └─────
508    with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
id                                         └───────────┘                       └──────────────────┘
src    └───────────┘└─────────────┘└┘└────┘└───────────┘   └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
typ    └───────────┘└─────────────┘└┘└────┘└───────────┘└┘└────┘└┘└──────┘└┘└──────────────────┘└┘
doc    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
txt    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
par    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
pid              └────────────────────────┘                └──────────────────┘                    └┘
st   ─────────────────────────────┘└─────────────────────────────────────────────────────────────────┘└─┘
509    case red_left { have := trans h (lo_lt_hi hl_hs₁), simp [*] },
id                             └───┘   └──────┘ └────┘
src    └──────────────┘└──────┘└───┘  └──────┘      └┘└───────┘
typ    └──────────────┘└──────┘└───┘ └──────┘└────┘└┘└───────┘
doc    └──────────────┘└──────┘                     └┘└───────┘
txt    └──────────────┘└──────┘                     └┘└───────┘
par    └──────────────┘└──────┘                     └┘└───────┘
pid        └───────┘└────────┘                     └───────────┘
st   ────────────────┘└────────────────────────────────┘└─────────┘└┘
510    case red_right { have := trans h (lo_lt_hi hl), simp [*] }
id                              └───┘   └──────┘ └┘
src    └───────────────┘└──────┘└───┘  └──────┘  └┘└───────┘└┘
typ    └───────────────┘└──────┘└───┘ └──────┘└┘└┘└───────┘└┘
doc    └───────────────┘└──────┘                 └┘└───────┘└┘
txt    └───────────────┘└──────┘                 └┘└───────┘└┘
par    └───────────────┘└──────┘                 └┘└───────┘└┘
pid        └────────┘└────────┘                 └───────────┘
st   ─────────────────┘└────────────────────────────┘└─────────┘
511  end
st   └─┘
512  
513  lemma find_balance2_node_lt {s t x y lo hi}
514                              (h : lt x y)
id                                    └┘  
typ                                   └┘  
515                              (ht : is_searchable lt t (some y) hi)
id                                     └───────────┘ └┘   └──┘   └┘
src                                    └───────────┘       └──┘
typ                                    └───────────┘ └┘   └──┘   └┘
516                              (hs : is_searchable lt s lo (some y))
id                                     └───────────┘ └┘  └┘  └──┘ 
src                                    └───────────┘          └──┘
typ                                    └───────────┘ └┘  └┘  └──┘ 
517                              (hne : t ≠ leaf . ins_ne_leaf_tac)
id                                        └──┘ 
src                                        └──┘ 
typ                                       └──┘ 
doc                                       
518                              : find lt (balance2_node t y s) x = find lt s x :=
id                                 └──┘ └┘  └───────────┘       └──┘ └┘  
src                                └──┘     └───────────┘           └──┘
typ                                └──┘ └┘  └───────────┘       └──┘ └┘  
519  begin
st   └─────
520    cases t; simp [balance2_node],
id                   └───────────┘
src    └────┘   └────┘└───────────┘
typ    └────┘  └────┘└───────────┘
doc    └────┘   └────┘             
txt    └────┘   └────┘             
par    └────┘   └────┘             
pid                             
st   ──────────────────────────────┘└─
521    all_goals { intros, is_searchable_tactic, apply find_balance2_lt, assumption' }
id                         └──────────────────┘        └──────────────┘
src    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└──────────────┘└┘└──────────┘└┘
typ    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└──────────────┘└┘└──────────┘└┘
doc    └──────────┘└────┘└┘                    └┘└────┘                └┘└──────────┘└┘
txt    └──────────┘└────┘└┘                    └┘└────┘                └┘└──────────┘└┘
par    └──────────┘└────┘└┘└──────────────────┘└┘└────┘                └┘└──────────┘└┘
pid             └─────────┘                    └──────┘                └─────────────┘
st   ────────────┘└───────────────────────────┘└──────────────────────┘└────────────┘
522  end
st   └─┘
523  
524  lemma find_balance2_gt {l v r t x y lo hi}
525                         (h :  lt y x)
id                                └┘  
typ                               └┘  
526                         (hl : is_searchable lt l (some y) (some v))
id                                └───────────┘ └┘   └──┘    └──┘ 
src                               └───────────┘       └──┘     └──┘
typ                               └───────────┘ └┘   └──┘    └──┘ 
527                         (hr : is_searchable lt r (some v) hi)
id                                └───────────┘ └┘   └──┘   └┘
src                               └───────────┘       └──┘
typ                               └───────────┘ └┘   └──┘   └┘
528                         (ht : is_searchable lt t lo (some y))
id                                └───────────┘ └┘  └┘  └──┘ 
src                               └───────────┘          └──┘
typ                               └───────────┘ └┘  └┘  └──┘ 
529                         : find lt (balance2 l v r y t) x = find lt (red_node l v r) x :=
id                            └──┘ └┘  └──────┘         └──┘ └┘  └──────┘     
src                           └──┘     └──────┘               └──┘     └──────┘
typ                           └──┘ └┘  └──────┘         └──┘ └┘  └──────┘     
530  begin
st   └─────
531    with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
id                                         └───────────┘                       └──────────────────┘
src    └───────────┘└─────────────┘└┘└────┘└───────────┘   └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
typ    └───────────┘└─────────────┘└┘└────┘└───────────┘└┘└────┘└┘└──────┘└┘└──────────────────┘└┘
doc    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
txt    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
par    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
pid              └────────────────────────┘                └──────────────────┘                    └┘
st   ─────────────────────────────┘└─────────────────────────────────────────────────────────────────┘└─┘
532    case red_left : _ val _ z {
src    └───────────────────────────
typ    └───────────────────────────
doc    └───────────────────────────
txt    └───────────────────────────
par    └───────────────────────────
pid        └───────┘└──────────┘└──
st   ────────────────────────────┘
533      with_cases { apply weak_trichotomous lt val x; intro h'; simp [*] },
id                          └───────────────┘ └┘ └─┘ 
src  ───┘└───────────┘└────┘└───────────────┘      └┘└──────┘└┘└───────┘└─
typ  ───┘└───────────┘└────┘└───────────────┘└┘└─┘└┘└──────┘└┘└───────┘└─
doc  ───┘└───────────┘└────┘                       └┘└──────┘└┘└───────┘└─
txt  ───┘└───────────┘└────┘                       └┘└──────┘└┘└───────┘└─
par  ───┘└───────────┘└────┘                       └┘└──────┘└┘└───────┘└─
pid  ──────────────────────┘                       └───────────────────────
st   ─────────────────────────────────────────────────────────────────────┘└─
534      case is_lt { apply weak_trichotomous lt z x; intros; simp [*] },
id                          └───────────────┘ └┘  
src  ────────────────┘└────┘└───────────────┘    └┘└────┘└┘└───────┘└──
typ  ────────────────┘└────┘└───────────────┘└┘└┘└────┘└┘└───────┘└──
doc  ────────────────┘└────┘                     └┘└────┘└┘└───────┘└──
txt  ────────────────┘└────┘                     └┘└────┘└┘└───────┘└──
par  ────────────────┘└────┘                     └┘└────┘└┘└───────┘└──
pid  ──────────────────────┘                     └─────────────────────
st   ───────────────┘└────────────────────────────────────────────────┘└─
535      case is_eqv { have : lt x z := lt_of_incomp_of_lt h'.swap (lo_lt_hi hl_hs₂), simp [*] },
id                            └┘      └────────────────┘ └─────┘  └──────┘ └────┘
src  ─────────────────┘└─────┘    └──┘└────────────────┘└─────┘ └──────┘      └┘└───────┘└──
typ  ─────────────────┘└─────┘└┘└──┘└────────────────┘└─────┘ └──────┘└────┘└┘└───────┘└──
doc  ─────────────────┘└─────┘    └──┘                                        └┘└───────┘└──
txt  ─────────────────┘└─────┘    └──┘                                        └┘└───────┘└──
par  ─────────────────┘└─────┘    └──┘                                        └┘└───────┘└──
pid  ────────────────────────┘    └──┘                                        └──────────────
st   ────────────────┘└────────────────────────────────────────────────────────────┘└─────────┘└─
536      case is_gt  { have := trans h' (lo_lt_hi hl_hs₂), simp [*] } },
id                             └───┘ └┘  └──────┘ └────┘
src  ─────────────────┘└──────┘└───┘   └──────┘      └┘└───────┘└─┘
typ  ─────────────────┘└──────┘└───┘└┘ └──────┘└────┘└┘└───────┘└─┘
doc  ─────────────────┘└──────┘                      └┘└───────┘└─┘
txt  ─────────────────┘└──────┘                      └┘└───────┘└─┘
par  ─────────────────┘└──────┘                      └┘└───────┘└─┘
pid  ─────────────────────────┘                      └─────────────┘
st   ────────────────┘└─────────────────────────────────┘└─────────┘└┘
537    case red_right : _ val {
src    └────────────────────────
typ    └────────────────────────
doc    └────────────────────────
txt    └────────────────────────
par    └────────────────────────
pid        └────────┘└──────┘└──
st   ─────────────────────────┘
538      apply weak_trichotomous lt val x; intros; simp [*] }
id             └───────────────┘ └┘ └─┘ 
src  ───┘└────┘└───────────────┘      └┘└────┘└┘└───────┘└┘
typ  ───┘└────┘└───────────────┘└┘└─┘└┘└────┘└┘└───────┘└┘
doc  ───┘└────┘                       └┘└────┘└┘└───────┘└┘
txt  ───┘└────┘                       └┘└────┘└┘└───────┘└┘
par  ───┘└────┘                       └┘└────┘└┘└───────┘└┘
pid  ─────────┘                       └──────────────────┘
st   ──────────────────────────────────────────────────────┘
539  end
st   └─┘
540  
541  lemma find_balance2_node_gt {s t x y lo hi}
542                              (h : lt y x)
id                                    └┘  
typ                                   └┘  
543                              (ht : is_searchable lt t (some y) hi)
id                                     └───────────┘ └┘   └──┘   └┘
src                                    └───────────┘       └──┘
typ                                    └───────────┘ └┘   └──┘   └┘
544                              (hs : is_searchable lt s lo (some y))
id                                     └───────────┘ └┘  └┘  └──┘ 
src                                    └───────────┘          └──┘
typ                                    └───────────┘ └┘  └┘  └──┘ 
545                              (hne : t ≠ leaf . ins_ne_leaf_tac)
id                                        └──┘ 
src                                        └──┘ 
typ                                       └──┘ 
doc                                       
546                              : find lt (balance2_node t y s) x = find lt t x :=
id                                 └──┘ └┘  └───────────┘       └──┘ └┘  
src                                └──┘     └───────────┘           └──┘
typ                                └──┘ └┘  └───────────┘       └──┘ └┘  
547  begin
st   └─────
548    cases t; simp [balance2_node],
id                   └───────────┘
src    └────┘   └────┘└───────────┘
typ    └────┘  └────┘└───────────┘
doc    └────┘   └────┘             
txt    └────┘   └────┘             
par    └────┘   └────┘             
pid                             
st   ──────────────────────────────┘└─
549    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
550    all_goals { intros, is_searchable_tactic, apply find_balance2_gt, assumption' }
id                         └──────────────────┘        └──────────────┘
src    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└──────────────┘└┘└──────────┘└┘
typ    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└──────────────┘└┘└──────────┘└┘
doc    └──────────┘└────┘└┘                    └┘└────┘                └┘└──────────┘└┘
txt    └──────────┘└────┘└┘                    └┘└────┘                └┘└──────────┘└┘
par    └──────────┘└────┘└┘└──────────────────┘└┘└────┘                └┘└──────────┘└┘
pid             └─────────┘                    └──────┘                └─────────────┘
st   ────────────┘└───────────────────────────┘└──────────────────────┘└────────────┘
551  end
st   └─┘
552  
553  lemma find_balance2_eqv {l v r t x y lo hi}
554                          (h : ¬ lt x y ∧ ¬ lt y x)
id                                 └┘     └┘  
src                                        
typ                                └┘     └┘  
555                          (hl : is_searchable lt l (some y) (some v))
id                                 └───────────┘ └┘   └──┘    └──┘ 
src                                └───────────┘       └──┘     └──┘
typ                                └───────────┘ └┘   └──┘    └──┘ 
556                          (hr : is_searchable lt r (some v) hi)
id                                 └───────────┘ └┘   └──┘   └┘
src                                └───────────┘       └──┘
typ                                └───────────┘ └┘   └──┘   └┘
557                          (ht : is_searchable lt t lo (some y))
id                                 └───────────┘ └┘  └┘  └──┘ 
src                                └───────────┘          └──┘
typ                                └───────────┘ └┘  └┘  └──┘ 
558                          : find lt (balance2 l v r y t) x = some y :=
id                             └──┘ └┘  └──────┘         └──┘ 
src                            └──┘     └──────┘               └──┘
typ                            └──┘ └┘  └──────┘         └──┘ 
559  begin
st   └─────
560    with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
id                                         └───────────┘                       └──────────────────┘
src    └───────────┘└─────────────┘└┘└────┘└───────────┘   └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
typ    └───────────┘└─────────────┘└┘└────┘└───────────┘└┘└────┘└┘└──────┘└┘└──────────────────┘└┘
doc    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
txt    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘                    └┘
par    └───────────┘└─────────────┘└┘└────┘                └┘└────┘└┘└──────┘└┘└──────────────────┘└┘
pid              └────────────────────────┘                └──────────────────┘                    └┘
st   ─────────────────────────────┘└─────────────────────────────────────────────────────────────────┘└─┘
561    case red_left { have := lt_of_incomp_of_lt h (lo_lt_hi hl_hs₁), simp [*] },
id                             └────────────────┘   └──────┘ └────┘
src    └──────────────┘└──────┘└────────────────┘  └──────┘      └┘└───────┘
typ    └──────────────┘└──────┘└────────────────┘ └──────┘└────┘└┘└───────┘
doc    └──────────────┘└──────┘                                  └┘└───────┘
txt    └──────────────┘└──────┘                                  └┘└───────┘
par    └──────────────┘└──────┘                                  └┘└───────┘
pid        └───────┘└────────┘                                  └───────────┘
st   ────────────────┘└─────────────────────────────────────────────┘└─────────┘└┘
562    case red_right { have := lt_of_incomp_of_lt h (lo_lt_hi hl), simp [*] }
id                              └────────────────┘   └──────┘ └┘
src    └───────────────┘└──────┘└────────────────┘  └──────┘  └┘└───────┘└┘
typ    └───────────────┘└──────┘└────────────────┘ └──────┘└┘└┘└───────┘└┘
doc    └───────────────┘└──────┘                              └┘└───────┘└┘
txt    └───────────────┘└──────┘                              └┘└───────┘└┘
par    └───────────────┘└──────┘                              └┘└───────┘└┘
pid        └────────┘└────────┘                              └───────────┘
st   ─────────────────┘└─────────────────────────────────────────┘└─────────┘
563  end
st   └─┘
564  
565  lemma find_balance2_node_eqv {t s x y lo hi}
566                               (h : ¬ lt x y ∧ ¬ lt y x)
id                                      └┘     └┘  
src                                             
typ                                     └┘     └┘  
567                               (ht : is_searchable lt t (some y) hi)
id                                      └───────────┘ └┘   └──┘   └┘
src                                     └───────────┘       └──┘
typ                                     └───────────┘ └┘   └──┘   └┘
568                               (hs : is_searchable lt s lo (some y))
id                                      └───────────┘ └┘  └┘  └──┘ 
src                                     └───────────┘          └──┘
typ                                     └───────────┘ └┘  └┘  └──┘ 
569                               (hne : t ≠ leaf . ins_ne_leaf_tac)
id                                         └──┘ 
src                                         └──┘ 
typ                                        └──┘ 
doc                                        
570                               : find lt (balance2_node t y s) x = some y :=
id                                  └──┘ └┘  └───────────┘       └──┘ 
src                                 └──┘     └───────────┘           └──┘
typ                                 └──┘ └┘  └───────────┘       └──┘ 
571  begin
st   └─────
572    cases t; simp [balance2_node],
id                   └───────────┘
src    └────┘   └────┘└───────────┘
typ    └────┘  └────┘└───────────┘
doc    └────┘   └────┘             
txt    └────┘   └────┘             
par    └────┘   └────┘             
pid                             
st   ──────────────────────────────┘└─
573    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
574    all_goals { intros, is_searchable_tactic, apply find_balance2_eqv, assumption' }
id                         └──────────────────┘        └───────────────┘
src    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└───────────────┘└┘└──────────┘└┘
typ    └──────────┘└────┘└┘└──────────────────┘└┘└────┘└───────────────┘└┘└──────────┘└┘
doc    └──────────┘└────┘└┘                    └┘└────┘                 └┘└──────────┘└┘
txt    └──────────┘└────┘└┘                    └┘└────┘                 └┘└──────────┘└┘
par    └──────────┘└────┘└┘└──────────────────┘└┘└────┘                 └┘└──────────┘└┘
pid             └─────────┘                    └──────┘                 └─────────────┘
st   ────────────┘└───────────────────────────┘└───────────────────────┘└────────────┘
575  end
st   └─┘
576  
577  lemma find_ins_of_disj {x y : α} {t : rbnode α} (hn : lt x y ∨ lt y x)
id                                        └────┘         └┘    └┘  
src                                        └────┘                 
typ                                       └────┘         └┘    └┘  
578                         : ∀ {lo hi}
id                               └┘ └┘
typ                              └┘ └┘
579                             (hs : is_searchable lt t lo hi)
id                                    └───────────┘ └┘  └┘ └┘
src                                   └───────────┘
typ                                   └───────────┘ └┘  └┘ └┘
580                             (hlt₁ : lift lt lo (some x))
id                                      └──┘ └┘ └┘  └──┘ 
src                                     └──┘        └──┘
typ                                     └──┘ └┘ └┘  └──┘ 
581                             (hlt₂ : lift lt (some x) hi),
id                                      └──┘ └┘  └──┘   └┘
src                                     └──┘     └──┘
typ                                     └──┘ └┘  └──┘   └┘
582                             find lt (ins lt t x) y = find lt t y :=
id                              └──┘ └┘  └─┘ └┘      └──┘ └┘  
src                             └──┘     └─┘            └──┘
typ                             └──┘ └┘  └─┘ └┘      └──┘ └┘  
583  begin
st   └─────
584    apply ins.induction lt t x; intros,
id           └───────────┘ └┘  
src    └────┘└───────────┘      └────┘
typ    └────┘└───────────┘└┘  └────┘
doc    └────┘                   └────┘
txt    └────┘                   └────┘
par    └────┘                   └────┘
pid                         
st   ───────────────────────────────────┘└─
585    { cases hn,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└──────┘└─
586      all_goals { simp [find, ins, cmp_using, *] } },
id                         └──┘  └─┘  └───────┘
src      └──────────┘└────┘└──┘└┘└─┘└┘└───────┘└───┘└┘
typ      └──────────┘└────┘└──┘└┘└─┘└┘└───────┘└───┘└┘
doc      └──────────┘└────┘    └┘   └┘         └───┘└┘
txt      └──────────┘└────┘    └┘   └┘         └───┘└┘
par      └──────────┘└────┘    └┘   └┘         └───┘└┘
pid               └───────┘    └┘   └┘         └────┘
st   ──────────────┘└──────────────────────────────┘└┘
587    all_goals { simp at hc, cases hs },
id                                   └┘
src    └──────────┘└────────┘└┘└────┘  
typ    └──────────┘└────────┘└┘└────┘└┘
doc    └──────────┘└────────┘└┘└────┘  
txt    └──────────┘└────────┘└┘└────┘  
par    └──────────┘└────────┘└┘└────┘  
pid             └───────────────────┘  └┘
st   ────────────┘└─────────┘└─────────┘└┘
588    { have := ih hs_hs₁ hlt₁ hc, simp_fi },
id               └┘ └────┘ └──┘ └┘  └─────┘
src      └──────┘                └─────┘
typ      └──────┘└┘└────┘└──┘└┘  └─────┘
doc      └──────┘            
txt      └──────┘            
par      └──────┘                └─────┘
pid      └───┘└─┘            
st   ───┘└───────────────────────┘└───────┘└─┘
589    { cases hn,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└──────┘└─
590      { have := lt_of_incomp_of_lt hc.symm hn,
id                 └────────────────┘ └─────┘ └┘
src        └──────┘└────────────────┘└─────┘
typ        └──────┘└────────────────┘└─────┘└┘
doc        └──────┘                         
txt        └──────┘                         
par        └──────┘                         
pid        └───┘└─┘                         
st   ─────┘└───────────────────────────────────┘└─
591        simp_fi },
id         └─────┘
src        └─────┘
typ        └─────┘
par        └─────┘
st   ────────────┘└─┘
592      { have := lt_of_lt_of_incomp hn hc,
id                 └────────────────┘ └┘ └┘
src        └──────┘└────────────────┘  
typ        └──────┘└────────────────┘└┘└┘
doc        └──────┘                    
txt        └──────┘                    
par        └──────┘                    
pid        └───┘└─┘                    
st   ─────────────────────────────────────┘└─
593        simp_fi } },
id         └─────┘
src        └─────┘
typ        └─────┘
par        └─────┘
st   ────────────┘└───┘
594    { have := ih hs_hs₂ hc hlt₂,
id               └┘ └────┘ └┘ └──┘
src      └──────┘          
typ      └──────┘└┘└────┘└┘└──┘
doc      └──────┘          
txt      └──────┘          
par      └──────┘          
pid      └───┘└─┘          
st   ───┘└───────────────────────┘└─
595      cases hn,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
596      { have := trans hc hn, simp_fi },
id                 └───┘ └┘ └┘  └─────┘
src        └──────┘└───┘      └─────┘
typ        └──────┘└───┘└┘└┘  └─────┘
doc        └──────┘       
txt        └──────┘       
par        └──────┘           └─────┘
pid        └───┘└─┘       
st   ─────┘└─────────────────┘└───────┘└─┘
597      { simp_fi } },
id         └─────┘
src        └─────┘
typ        └─────┘
par        └─────┘
st   ────────────┘└───┘
598    { have ih := ih hs_hs₁ hlt₁ hc,
id                  └┘ └────┘ └──┘ └┘
src      └─────────┘            
typ      └─────────┘└┘└────┘└──┘└┘
doc      └─────────┘            
txt      └─────────┘            
par      └─────────┘            
pid      └─────┘└─┘            
st   ───┘└──────────────────────────┘└─
599      cases hn,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
600      { cases hc' : cmp_using lt y y_1; simp at hc',
id                     └───────┘ └┘  └─┘
src        └────┘   └─┘└───────┘        └─────────┘
typ        └────┘   └─┘└───────┘└┘└─┘  └─────────┘
doc        └────┘   └─┘                 └─────────┘
txt        └────┘   └─┘                 └─────────┘
par        └────┘   └─┘                 └─────────┘
pid                └─┘                     └────┘
st   ─────┘└─────────────────────────────────────────┘└─
601        { have hsi := is_searchable_ins lt hs_hs₁ hlt₁ (trans_of lt hn hc'),
id                       └───────────────┘    └────┘ └──┘  └──────┘ └┘ └┘ └─┘
src          └──────────┘└───────────────┘             └──────┘       
typ          └──────────┘└───────────────┘  └────┘└──┘ └──────┘└┘└┘└─┘
doc          └──────────┘                                             
txt          └──────────┘                                             
par          └──────────┘                                             
pid          └──────┘└─┘                                             
st   ───────┘└───────────────────────────────────────────────────────────────┘└─
602          have := find_balance1_node_lt lt hc' hsi hs_hs₂,
id                   └───────────────────┘ └┘ └─┘ └─┘ └────┘
src          └──────┘└───────────────────┘        
typ          └──────┘└───────────────────┘└┘└─┘└─┘└────┘
doc          └──────┘                             
txt          └──────┘                             
par          └──────┘                             
pid          └───┘└─┘                             
st   ──────────────────────────────────────────────────────┘└─
603          simp_fi },
id           └─────┘
src          └─────┘
typ          └─────┘
par          └─────┘
st   ──────────────┘└─┘
604        { have hlt := lt_of_lt_of_incomp hn hc',
id                       └────────────────┘ └┘ └─┘
src          └──────────┘└────────────────┘  
typ          └──────────┘└────────────────┘└┘└─┘
doc          └──────────┘                    
txt          └──────────┘                    
par          └──────────┘                    
pid          └──────┘└─┘                    
st   ───────┘└───────────────────────────────────┘└─
605          have hsi := is_searchable_ins lt hs_hs₁ hlt₁ hlt,
id                       └───────────────┘ └┘ └────┘ └──┘ └─┘
src          └──────────┘└───────────────┘            
typ          └──────────┘└───────────────┘└┘└────┘└──┘└─┘
doc          └──────────┘                             
txt          └──────────┘                             
par          └──────────┘                             
pid          └──────┘└─┘                             
st   ───────────────────────────────────────────────────────┘└─
606          have := find_balance1_node_eqv lt hc' hsi hs_hs₂,
id                   └────────────────────┘ └┘ └─┘ └─┘ └────┘
src          └──────┘└────────────────────┘        
typ          └──────┘└────────────────────┘└┘└─┘└─┘└────┘
doc          └──────┘                              
txt          └──────┘                              
par          └──────┘                              
pid          └───┘└─┘                              
st   ───────────────────────────────────────────────────────┘└─
607          simp_fi },
id           └─────┘
src          └─────┘
typ          └─────┘
par          └─────┘
st   ──────────────┘└─┘
608        { have hsi := is_searchable_ins lt hs_hs₁ hlt₁ hc,
id                       └───────────────┘ └┘ └────┘ └──┘ └┘
src          └──────────┘└───────────────┘            
typ          └──────────┘└───────────────┘└┘└────┘└──┘└┘
doc          └──────────┘                             
txt          └──────────┘                             
par          └──────────┘                             
pid          └──────┘└─┘                             
st   ──────────────────────────────────────────────────────┘└─
609          have := find_balance1_node_gt lt hc' hsi hs_hs₂,
id                   └───────────────────┘ └┘ └─┘ └─┘ └────┘
src          └──────┘└───────────────────┘        
typ          └──────┘└───────────────────┘└┘└─┘└─┘└────┘
doc          └──────┘                             
txt          └──────┘                             
par          └──────┘                             
pid          └───┘└─┘                             
st   ──────────────────────────────────────────────────────┘└─
610          simp [*], simp_fi } },
id                     └─────┘
src          └──────┘  └─────┘
typ          └──────┘  └─────┘
doc          └──────┘
txt          └──────┘
par          └──────┘  └─────┘
pid              └─┘
st   ───────────────┘└───────┘└───┘
611      { have hlt := trans hn hc,
id                     └───┘ └┘ └┘
src        └──────────┘└───┘  
typ        └──────────┘└───┘└┘└┘
doc        └──────────┘       
txt        └──────────┘       
par        └──────────┘       
pid        └──────┘└─┘       
st   ────────────────────────────┘└─
612        have hsi := is_searchable_ins lt hs_hs₁ hlt₁ hc,
id                     └───────────────┘ └┘ └────┘ └──┘ └┘
src        └──────────┘└───────────────┘            
typ        └──────────┘└───────────────┘└┘└────┘└──┘└┘
doc        └──────────┘                             
txt        └──────────┘                             
par        └──────────┘                             
pid        └──────┘└─┘                             
st   ────────────────────────────────────────────────────┘└─
613        have := find_balance1_node_lt lt hlt hsi hs_hs₂,
id                 └───────────────────┘ └┘ └─┘ └─┘ └────┘
src        └──────┘└───────────────────┘        
typ        └──────┘└───────────────────┘└┘└─┘└─┘└────┘
doc        └──────┘                             
txt        └──────┘                             
par        └──────┘                             
pid        └───┘└─┘                             
st   ────────────────────────────────────────────────────┘└─
614        simp_fi } },
id         └─────┘
src        └─────┘
typ        └─────┘
par        └─────┘
st   ────────────┘└───┘
615    { have := ih hs_hs₁ hlt₁ hc, simp_fi },
id               └┘ └────┘ └──┘ └┘  └─────┘
src      └──────┘                └─────┘
typ      └──────┘└┘└────┘└──┘└┘  └─────┘
doc      └──────┘            
txt      └──────┘            
par      └──────┘                └─────┘
pid      └───┘└─┘            
st   ───┘└───────────────────────┘└───────┘└─┘
616    { cases hn,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└──────┘└─
617      { have := lt_of_incomp_of_lt hc.swap hn, simp_fi },
id                 └────────────────┘ └─────┘ └┘  └─────┘
src        └──────┘└────────────────┘└─────┘    └─────┘
typ        └──────┘└────────────────┘└─────┘└┘  └─────┘
doc        └──────┘                         
txt        └──────┘                         
par        └──────┘                             └─────┘
pid        └───┘└─┘                         
st   ─────┘└───────────────────────────────────┘└───────┘└─┘
618      { have := lt_of_lt_of_incomp hn hc, simp_fi } },
id                 └────────────────┘ └┘ └┘  └─────┘
src        └──────┘└────────────────┘      └─────┘
typ        └──────┘└────────────────┘└┘└┘  └─────┘
doc        └──────┘                    
txt        └──────┘                    
par        └──────┘                        └─────┘
pid        └───┘└─┘                    
st   ─────────────────────────────────────┘└───────┘└───┘
619    { have ih := ih hs_hs₂ hc hlt₂,
id                  └┘ └────┘ └┘ └──┘
src      └─────────┘          
typ      └─────────┘└┘└────┘└┘└──┘
doc      └─────────┘          
txt      └─────────┘          
par      └─────────┘          
pid      └─────┘└─┘          
st   ───┘└──────────────────────────┘└─
620      cases hn,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
621      { have hlt := trans hc hn, simp_fi,
id                     └───┘ └┘ └┘  └─────┘
src        └──────────┘└───┘      └─────┘
typ        └──────────┘└───┘└┘└┘  └─────┘
doc        └──────────┘       
txt        └──────────┘       
par        └──────────┘           └─────┘
pid        └──────┘└─┘       
st   ─────┘└─────────────────────┘└───────┘└─
622        have hsi := is_searchable_ins lt hs_hs₂ hc hlt₂,
id                     └───────────────┘ └┘ └────┘ └┘ └──┘
src        └──────────┘└───────────────┘          
typ        └──────────┘└───────────────┘└┘└────┘└┘└──┘
doc        └──────────┘                           
txt        └──────────┘                           
par        └──────────┘                           
pid        └──────┘└─┘                           
st   ────────────────────────────────────────────────────┘└─
623        have := find_balance2_node_gt lt hlt hsi hs_hs₁,
id                 └───────────────────┘ └┘ └─┘ └─┘ └────┘
src        └──────┘└───────────────────┘        
typ        └──────┘└───────────────────┘└┘└─┘└─┘└────┘
doc        └──────┘                             
txt        └──────┘                             
par        └──────┘                             
pid        └───┘└─┘                             
st   ────────────────────────────────────────────────────┘└─
624        simp_fi },
id         └─────┘
src        └─────┘
typ        └─────┘
par        └─────┘
st   ────────────┘└─┘
625      { simp_fi,
id         └─────┘
src        └─────┘
typ        └─────┘
par        └─────┘
st   ────────────┘└─
626        cases hc' : cmp_using lt y y_1; simp at hc',
id                     └───────┘ └┘  └─┘
src        └────┘   └─┘└───────┘        └─────────┘
typ        └────┘   └─┘└───────┘└┘└─┘  └─────────┘
doc        └────┘   └─┘                 └─────────┘
txt        └────┘   └─┘                 └─────────┘
par        └────┘   └─┘                 └─────────┘
pid                └─┘                     └────┘
st   ────────────────────────────────────────────────┘└─
627        { have hsi := is_searchable_ins lt hs_hs₂ hc hlt₂,
id                       └───────────────┘ └┘ └────┘ └┘ └──┘
src          └──────────┘└───────────────┘          
typ          └──────────┘└───────────────┘└┘└────┘└┘└──┘
doc          └──────────┘                           
txt          └──────────┘                           
par          └──────────┘                           
pid          └──────┘└─┘                           
st   ───────┘└─────────────────────────────────────────────┘└─
628          have := find_balance2_node_lt lt hc' hsi hs_hs₁,
id                   └───────────────────┘ └┘ └─┘ └─┘ └────┘
src          └──────┘└───────────────────┘        
typ          └──────┘└───────────────────┘└┘└─┘└─┘└────┘
doc          └──────┘                             
txt          └──────┘                             
par          └──────┘                             
pid          └───┘└─┘                             
st   ──────────────────────────────────────────────────────┘└─
629          simp_fi },
id           └─────┘
src          └─────┘
typ          └─────┘
par          └─────┘
st   ──────────────┘└─┘
630        { have hlt := lt_of_incomp_of_lt hc'.swap hn,
id                       └────────────────┘ └──────┘ └┘
src          └──────────┘└────────────────┘└──────┘
typ          └──────────┘└────────────────┘└──────┘└┘
doc          └──────────┘                          
txt          └──────────┘                          
par          └──────────┘                          
pid          └──────┘└─┘                          
st   ───────┘└────────────────────────────────────────┘└─
631          have hsi := is_searchable_ins lt hs_hs₂ hlt hlt₂,
id                       └───────────────┘ └┘ └────┘ └─┘ └──┘
src          └──────────┘└───────────────┘           
typ          └──────────┘└───────────────┘└┘└────┘└─┘└──┘
doc          └──────────┘                            
txt          └──────────┘                            
par          └──────────┘                            
pid          └──────┘└─┘                            
st   ───────────────────────────────────────────────────────┘└─
632          have := find_balance2_node_eqv lt hc' hsi hs_hs₁,
id                   └────────────────────┘ └┘ └─┘ └─┘ └────┘
src          └──────┘└────────────────────┘        
typ          └──────┘└────────────────────┘└┘└─┘└─┘└────┘
doc          └──────┘                              
txt          └──────┘                              
par          └──────┘                              
pid          └───┘└─┘                              
st   ───────────────────────────────────────────────────────┘└─
633          simp_fi },
id           └─────┘
src          └─────┘
typ          └─────┘
par          └─────┘
st   ──────────────┘└─┘
634        { have hsi := is_searchable_ins lt hs_hs₂ hc hlt₂,
id                       └───────────────┘ └┘ └────┘ └┘ └──┘
src          └──────────┘└───────────────┘          
typ          └──────────┘└───────────────┘└┘└────┘└┘└──┘
doc          └──────────┘                           
txt          └──────────┘                           
par          └──────────┘                           
pid          └──────┘└─┘                           
st   ──────────────────────────────────────────────────────┘└─
635          have := find_balance2_node_gt lt hc' hsi hs_hs₁,
id                   └───────────────────┘ └┘ └─┘ └─┘ └────┘
src          └──────┘└───────────────────┘        
typ          └──────┘└───────────────────┘└┘└─┘└─┘└────┘
doc          └──────┘                             
txt          └──────┘                             
par          └──────┘                             
pid          └───┘└─┘                             
st   ──────────────────────────────────────────────────────┘└─
636          simp_fi } } },
id           └─────┘
src          └─────┘
typ          └─────┘
par          └─────┘
st   ──────────────┘└─────┘
637    { cases hn,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
638      { have := trans hc hn,
id                 └───┘ └┘ └┘
src        └──────┘└───┘  
typ        └──────┘└───┘└┘└┘
doc        └──────┘       
txt        └──────┘       
par        └──────┘       
pid        └───┘└─┘       
st   ─────┘└─────────────────┘└─
639        have := ih hs_hs₂ hc hlt₂,
id                 └┘ └────┘ └┘ └──┘
src        └──────┘          
typ        └──────┘└┘└────┘└┘└──┘
doc        └──────┘          
txt        └──────┘          
par        └──────┘          
pid        └───┘└─┘          
st   ──────────────────────────────┘└─
640        simp_fi },
id         └─────┘
src        └─────┘
typ        └─────┘
par        └─────┘
st   ────────────┘└─┘
641      { have ih := ih hs_hs₂ hc hlt₂,
id                    └┘ └────┘ └┘ └──┘
src        └─────────┘          
typ        └─────────┘└┘└────┘└┘└──┘
doc        └─────────┘          
txt        └─────────┘          
par        └─────────┘          
pid        └─────┘└─┘          
st   ─────────────────────────────────┘└─
642        simp_fi } }
id         └─────┘
src        └─────┘
typ        └─────┘
par        └─────┘
st   ────────────┘└────
643  end
st   ──┘
644  
645  end find_ins_of_not_eqv
646  
647  lemma find_insert_of_disj [is_strict_weak_order α lt] {x y : α} {t : rbnode α} (hd : lt x y ∨ lt y x) : is_searchable lt t none none → find lt (insert lt t x) y = find lt t y :=
id                              └──────────────────┘  └┘                └────┘         └┘    └┘      └───────────┘ └┘  └──┘ └──┘   └──┘ └┘  └────┘ └┘      └──┘ └┘  
src                             └──────────────────┘                      └────┘                            └───────────┘      └──┘ └──┘   └──┘     └────┘            └──┘
typ                             └──────────────────┘  └┘                └────┘         └┘    └┘      └───────────┘ └┘  └──┘ └──┘   └──┘ └┘  └────┘ └┘      └──┘ └┘  
648  begin
st   └─────
649    intro hs,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid         └─┘
st   ─────────┘└─
650    simp [insert, find_mk_insert_result],
id           └────┘  └───────────────────┘
src    └────┘└────┘└┘└───────────────────┘
typ    └────┘└────┘└┘└───────────────────┘
doc    └────┘      └┘                     
txt    └────┘      └┘                     
par    └────┘      └┘                     
pid              └┘                     
st   ─────────────────────────────────────┘└─
651    apply find_ins_of_disj lt hd hs; simp
id           └──────────────┘ └┘ └┘ └┘
src    └────┘└──────────────┘        └───┘
typ    └────┘└──────────────┘└┘└┘└┘  └───┘
doc    └────┘                        └───┘
txt    └────┘                        └───┘
par    └────┘                        └───┘
pid                                     
st   ───────────────────────────────────────┘
652  end
st   └─┘
653  
654  lemma find_insert_of_not_eqv [is_strict_weak_order α lt] {x y : α} {t : rbnode α} (hn : ¬ x ≈[lt] y) : is_searchable lt t none none → find lt (insert lt t x) y = find lt t y :=
id                                 └──────────────────┘  └┘                └────┘           └┘└┘     └───────────┘ └┘  └──┘ └──┘   └──┘ └┘  └────┘ └┘      └──┘ └┘  
src                                └──────────────────┘                      └────┘             └┘        └───────────┘      └──┘ └──┘   └──┘     └────┘            └──┘
typ                                └──────────────────┘  └┘                └────┘           └┘└┘     └───────────┘ └┘  └──┘ └──┘   └──┘ └┘  └────┘ └┘      └──┘ └┘  
655  begin
st   └─────
656    intro hs,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid         └─┘
st   ─────────┘└─
657    simp [insert, find_mk_insert_result],
id           └────┘  └───────────────────┘
src    └────┘└────┘└┘└───────────────────┘
typ    └────┘└────┘└┘└───────────────────┘
doc    └────┘      └┘                     
txt    └────┘      └┘                     
par    └────┘      └┘                     
pid              └┘                     
st   ─────────────────────────────────────┘└─
658    have he : lt x y ∨ lt y x, {
id                       └┘  
src    └────────┘       
typ    └────────┘    └┘
doc    └────────┘        
txt    └────────┘        
par    └────────┘        
pid    └─────┘└─┘        
st   ──────────────────────────┘└──┘
659      simp [strict_weak_order.equiv, decidable.not_and_iff_or_not, decidable.not_not_iff] at hn,
id             └─────────────────────┘  └──────────────────────────┘  └───────────────────┘
src      └────┘└─────────────────────┘└┘└──────────────────────────┘└┘└───────────────────┘└─────┘
typ      └────┘└─────────────────────┘└┘└──────────────────────────┘└┘└───────────────────┘└─────┘
doc      └────┘                       └┘                            └┘                     └─────┘
txt      └────┘                       └┘                            └┘                     └─────┘
par      └────┘                       └┘                            └┘                     └─────┘
pid                                 └┘                            └┘                     └───┘
st   └───────────────────────────────────────────────────────────────────────────────────────────┘└─
660      assumption },
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid                
st   ──────────────┘└┘
661    apply find_ins_of_disj lt he hs; simp
id           └──────────────┘ └┘ └┘ └┘
src    └────┘└──────────────┘        └───┘
typ    └────┘└──────────────┘└┘└┘└┘  └───┘
doc    └────┘                        └───┘
txt    └────┘                        └───┘
par    └────┘                        └───┘
pid                                     
st   ───────────────────────────────────────┘
662  end
st   └─┘
663  
664  end membership_lemmas
665  
666  section is_red_black
667  variables {α : Type u}
668  open nat color
669  
670  inductive is_bad_red_black : rbnode α → nat → Prop
id                                └────┘     └─┘
src                               └────┘     └─┘
typ                               └────┘     └─┘
671  | bad_red   {c₁ c₂ n l r v} (rb_l : is_red_black l c₁ n) (rb_r : is_red_black r c₂ n) : is_bad_red_black (red_node l v r) n
id                └┘ └┘              └──────────┘  └┘           └──────────┘  └┘                       └──────┘     
src                                      └──────────┘                 └──────────┘                             └──────┘
typ               └┘ └┘              └──────────┘  └┘           └──────────┘  └┘                       └──────┘     
672  
673  lemma balance1_rb {l r t : rbnode α} {y v : α} {c_l c_r c_t n} : is_red_black l c_l n → is_red_black r c_r n → is_red_black t c_t n → ∃ c, is_red_black (balance1 l y r v t) c (succ n) :=
id                              └────┘                              └──────────┘  └─┘    └──────────┘  └─┘    └──────────┘  └─┘      └──────────┘  └──────┘         └──┘ 
src                             └────┘                                └──────────┘           └──────────┘           └──────────┘              └──────────┘  └──────┘               └──┘
typ                             └────┘                              └──────────┘  └─┘    └──────────┘  └─┘    └──────────┘  └─┘      └──────────┘  └──────┘         └──┘ 
674  by intros h₁ h₂ _; cases h₁; cases h₂; repeat { assumption <|> constructor }
id                            └┘        └┘
src     └────────────┘  └────┘    └────┘    └───────┘└─────────┘└──┘└──────────┘└─
typ     └────────────┘  └────┘└┘  └────┘└┘  └───────┘└─────────┘└──┘└──────────┘└─
doc     └────────────┘  └────┘    └────┘    └───────┘└─────────┘└──┘└──────────┘└─
txt     └────────────┘  └────┘    └────┘    └───────┘└─────────┘└──┘└──────────┘└─
par     └────────────┘  └────┘    └────┘    └───────┘└─────────┘└──┘└──────────┘└─
pid           └──────┘                          └─────────────────────────────┘
st     └───────────────────────────────────────────┘└──────────────────────────┘
675  
src  
typ  
doc  
txt  
par  
pid  
st   
676  lemma balance2_rb {l r t : rbnode α} {y v : α} {c_l c_r c_t n} : is_red_black l c_l n → is_red_black r c_r n → is_red_black t c_t n → ∃ c, is_red_black (balance2 l y r v t) c (succ n) :=
id                              └────┘                              └──────────┘  └─┘    └──────────┘  └─┘    └──────────┘  └─┘      └──────────┘  └──────┘         └──┘ 
src                             └────┘                                └──────────┘           └──────────┘           └──────────┘              └──────────┘  └──────┘               └──┘
typ                             └────┘                              └──────────┘  └─┘    └──────────┘  └─┘    └──────────┘  └─┘      └──────────┘  └──────┘         └──┘ 
677  by intros h₁ h₂ _; cases h₁; cases h₂; repeat { assumption <|> constructor }
id                            └┘        └┘
src     └────────────┘  └────┘    └────┘    └───────┘└─────────┘└──┘└──────────┘└─
typ     └────────────┘  └────┘└┘  └────┘└┘  └───────┘└─────────┘└──┘└──────────┘└─
doc     └────────────┘  └────┘    └────┘    └───────┘└─────────┘└──┘└──────────┘└─
txt     └────────────┘  └────┘    └────┘    └───────┘└─────────┘└──┘└──────────┘└─
par     └────────────┘  └────┘    └────┘    └───────┘└─────────┘└──┘└──────────┘└─
pid           └──────┘                          └─────────────────────────────┘
st     └───────────────────────────────────────────┘└──────────────────────────┘
678  
src  
typ  
doc  
txt  
par  
pid  
st   
679  lemma balance1_node_rb {t s : rbnode α} {y : α} {c n} : is_bad_red_black t n → is_red_black s c n → ∃ c, is_red_black (balance1_node t y s) c (succ n) :=
id                                 └────┘                  └──────────────┘     └──────────┘        └──────────┘  └───────────┘       └──┘ 
src                                └────┘                    └──────────────┘       └──────────┘            └──────────┘  └───────────┘           └──┘
typ                                └────┘                  └──────────────┘     └──────────┘        └──────────┘  └───────────┘       └──┘ 
680  by intros h _; cases h; simp [balance1_node]; apply balance1_rb; assumption'
id                                └───────────┘         └─────────┘
src     └────────┘  └────┘   └────┘└───────────┘  └────┘└─────────┘  └───────────
typ     └────────┘  └────┘  └────┘└───────────┘  └────┘└─────────┘  └───────────
doc     └────────┘  └────┘   └────┘               └────┘             └───────────
txt     └────────┘  └────┘   └────┘               └────┘             └───────────
par     └────────┘  └────┘   └────┘               └────┘             └───────────
pid           └──┘                                                          
st     └──────────────────────────────────────────────────────────────────────────
681  
src  
typ  
doc  
txt  
par  
pid  
st   
682  lemma balance2_node_rb {t s : rbnode α} {y : α} {c n} : is_bad_red_black t n → is_red_black s c n → ∃ c, is_red_black (balance2_node t y s) c (succ n) :=
id                                 └────┘                  └──────────────┘     └──────────┘        └──────────┘  └───────────┘       └──┘ 
src                                └────┘                    └──────────────┘       └──────────┘            └──────────┘  └───────────┘           └──┘
typ                                └────┘                  └──────────────┘     └──────────┘        └──────────┘  └───────────┘       └──┘ 
683  by intros h _; cases h; simp [balance2_node]; apply balance2_rb; assumption'
id                                └───────────┘         └─────────┘
src     └────────┘  └────┘   └────┘└───────────┘  └────┘└─────────┘  └───────────
typ     └────────┘  └────┘  └────┘└───────────┘  └────┘└─────────┘  └───────────
doc     └────────┘  └────┘   └────┘               └────┘             └───────────
txt     └────────┘  └────┘   └────┘               └────┘             └───────────
par     └────────┘  └────┘   └────┘               └────┘             └───────────
pid           └──┘                                                          
st     └──────────────────────────────────────────────────────────────────────────
684  
src  
typ  
doc  
txt  
par  
pid  
st   
685  def ins_rb_result : rbnode α → color → nat → Prop
id                       └────┘   └───┘   └─┘
src                      └────┘     └───┘   └─┘
typ                      └────┘   └───┘   └─┘
686  | t red   n := is_bad_red_black t n
id      └─┘       └──────────────┘
src      └─┘        └──────────────┘
typ     └─┘       └──────────────┘
687  | t black n := ∃ c, is_red_black t c n
id      └───┘       └──────────┘   
src      └───┘         └──────────┘
typ     └───┘       └──────────┘   
688  
689  variables {lt : α → α → Prop} [decidable_rel lt]
id                                 └───────────┘
src                                 └───────────┘
typ                                └───────────┘
690  
691  lemma of_get_color_eq_red {t : rbnode α} {c n} : get_color t = red → is_red_black t c n → c = red :=
id                                  └────┘           └───────┘   └─┘   └──────────┘        └─┘
src                                 └────┘            └───────┘    └─┘   └──────────┘            └─┘
typ                                 └────┘           └───────┘   └─┘   └──────────┘        └─┘
692  begin intros h₁ h₂, cases h₂; simp [get_color] at h₁; contradiction end
id                             └┘        └───────┘
src        └──────────┘  └────┘    └────┘└───────┘└─────┘  └────────────┘
typ        └──────────┘  └────┘└┘  └────┘└───────┘└─────┘  └────────────┘
doc        └──────────┘  └────┘    └────┘         └─────┘  └────────────┘
txt        └──────────┘  └────┘    └────┘         └─────┘  └────────────┘
par        └──────────┘  └────┘    └────┘         └─────┘  └────────────┘
pid              └────┘                        └───┘               
st   └────────────────┘└────────────────────────────────────────────────┘└─┘
693  
694  lemma of_get_color_ne_red {t : rbnode α} {c n} : get_color t ≠ red → is_red_black t c n → c = black :=
id                                  └────┘           └───────┘   └─┘   └──────────┘        └───┘
src                                 └────┘            └───────┘    └─┘   └──────────┘            └───┘
typ                                 └────┘           └───────┘   └─┘   └──────────┘        └───┘
695  begin intros h₁ h₂, cases h₂; simp [get_color] at h₁; contradiction end
id                             └┘        └───────┘
src        └──────────┘  └────┘    └────┘└───────┘└─────┘  └────────────┘
typ        └──────────┘  └────┘└┘  └────┘└───────┘└─────┘  └────────────┘
doc        └──────────┘  └────┘    └────┘         └─────┘  └────────────┘
txt        └──────────┘  └────┘    └────┘         └─────┘  └────────────┘
par        └──────────┘  └────┘    └────┘         └─────┘  └────────────┘
pid              └────┘                        └───┘               
st   └────────────────┘└────────────────────────────────────────────────┘└─┘
696  
697  variable (lt)
698  
699  lemma ins_rb {t : rbnode α} (x) : ∀ {c n} (h : is_red_black t c n), ins_rb_result (ins lt t x) c n :=
id                     └────┘                    └──────────┘      └───────────┘  └─┘ └┘     
src                    └────┘                       └──────────┘         └───────────┘  └─┘
typ                    └────┘                    └──────────┘      └───────────┘  └─┘ └┘     
700  begin
st   └─────
701    apply ins.induction lt t x; intros; cases h; simp [ins, *, ins_rb_result],
id           └───────────┘ └┘                          └─┘     └───────────┘
src    └────┘└───────────┘      └────┘  └────┘   └────┘└─┘└───┘└───────────┘
typ    └────┘└───────────┘└┘  └────┘  └────┘  └────┘└─┘└───┘└───────────┘
doc    └────┘                   └────┘  └────┘   └────┘   └───┘             
txt    └────┘                   └────┘  └────┘   └────┘   └───┘             
par    └────┘                   └────┘  └────┘   └────┘   └───┘             
pid                                                   └───┘             
st   ──────────────────────────────────────────────────────────────────────────┘└─
702    { repeat { constructor } },
src      └───────┘└──────────┘└┘
typ      └───────┘└──────────┘└┘
doc      └───────┘└──────────┘└┘
txt      └───────┘└──────────┘└┘
par      └───────┘└──────────┘└┘
pid            └──────────────┘
st   ───┘└───────────────────┘└┘
703    { specialize ih h_rb_l, cases ih, constructor; assumption },
id                  └┘ └────┘        └┘
src      └─────────┘          └────┘    └─────────┘  └─────────┘
typ      └─────────┘└┘└────┘  └────┘└┘  └─────────┘  └─────────┘
doc      └─────────┘          └────┘    └─────────┘  └─────────┘
txt      └─────────┘          └────┘    └─────────┘  └─────────┘
par      └─────────┘          └────┘    └─────────┘  └─────────┘
pid                                                          
st   ───┘└──────────────────┘└────────┘└────────────────────────┘└┘
704    { constructor; assumption },
src      └─────────┘  └─────────┘
typ      └─────────┘  └─────────┘
doc      └─────────┘  └─────────┘
txt      └─────────┘  └─────────┘
par      └─────────┘  └─────────┘
pid                             
st   ───┘└──────────────────────┘└┘
705    { specialize ih h_rb_r, cases ih, constructor; assumption },
id                  └┘ └────┘        └┘
src      └─────────┘          └────┘    └─────────┘  └─────────┘
typ      └─────────┘└┘└────┘  └────┘└┘  └─────────┘  └─────────┘
doc      └─────────┘          └────┘    └─────────┘  └─────────┘
txt      └─────────┘          └────┘    └─────────┘  └─────────┘
par      └─────────┘          └────┘    └─────────┘  └─────────┘
pid                                                          
st   ───┘└──────────────────┘└────────┘└────────────────────────┘└┘
706    { specialize ih h_rb_l,
id                  └┘ └────┘
src      └─────────┘  
typ      └─────────┘└┘└────┘
doc      └─────────┘  
txt      └─────────┘  
par      └─────────┘  
pid                  
st   ───┘└──────────────────┘└─
707      have := of_get_color_eq_red hr h_rb_l, subst h_c₁,
id               └─────────────────┘ └┘ └────┘        └──┘
src      └──────┘└─────────────────┘          └────┘
typ      └──────┘└─────────────────┘└┘└────┘  └────┘└──┘
doc      └──────┘                             └────┘
txt      └──────┘                             └────┘
par      └──────┘                             └────┘
pid      └───┘└─┘                                  
st   ────────────────────────────────────────┘└──────────┘└─
708      simp [ins_rb_result] at ih,
id             └───────────┘
src      └────┘└───────────┘└─────┘
typ      └────┘└───────────┘└─────┘
doc      └────┘             └─────┘
txt      └────┘             └─────┘
par      └────┘             └─────┘
pid                       └───┘
st   ─────────────────────────────┘└─
709      apply balance1_node_rb; assumption },
id             └──────────────┘
src      └────┘└──────────────┘  └─────────┘
typ      └────┘└──────────────┘  └─────────┘
doc      └────┘                  └─────────┘
txt      └────┘                  └─────────┘
par      └────┘                  └─────────┘
pid                                       
st   ──────────────────────────────────────┘└┘
710    { specialize ih h_rb_l,
id                  └┘ └────┘
src      └─────────┘  
typ      └─────────┘└┘└────┘
doc      └─────────┘  
txt      └─────────┘  
par      └─────────┘  
pid                  
st   ───┘└──────────────────┘└─
711      have := of_get_color_ne_red hnr h_rb_l, subst h_c₁,
id               └─────────────────┘ └─┘ └────┘        └──┘
src      └──────┘└─────────────────┘           └────┘
typ      └──────┘└─────────────────┘└─┘└────┘  └────┘└──┘
doc      └──────┘                              └────┘
txt      └──────┘                              └────┘
par      └──────┘                              └────┘
pid      └───┘└─┘                                   
st   ─────────────────────────────────────────┘└──────────┘└─
712      simp [ins_rb_result] at ih, cases ih,
id             └───────────┘               └┘
src      └────┘└───────────┘└─────┘  └────┘
typ      └────┘└───────────┘└─────┘  └────┘└┘
doc      └────┘             └─────┘  └────┘
txt      └────┘             └─────┘  └────┘
par      └────┘             └─────┘  └────┘
pid                       └───┘       
st   ─────────────────────────────┘└────────┘└─
713      constructor, constructor; assumption },
src      └─────────┘  └─────────┘  └─────────┘
typ      └─────────┘  └─────────┘  └─────────┘
doc      └─────────┘  └─────────┘  └─────────┘
txt      └─────────┘  └─────────┘  └─────────┘
par      └─────────┘  └─────────┘  └─────────┘
pid                                          
st   ──────────────┘└────────────────────────┘└┘
714    { constructor, constructor; assumption },
src      └─────────┘  └─────────┘  └─────────┘
typ      └─────────┘  └─────────┘  └─────────┘
doc      └─────────┘  └─────────┘  └─────────┘
txt      └─────────┘  └─────────┘  └─────────┘
par      └─────────┘  └─────────┘  └─────────┘
pid                                          
st   ───┘└─────────┘└────────────────────────┘└┘
715    { specialize ih h_rb_r,
id                  └┘ └────┘
src      └─────────┘  
typ      └─────────┘└┘└────┘
doc      └─────────┘  
txt      └─────────┘  
par      └─────────┘  
pid                  
st   ───┘└──────────────────┘└─
716      have := of_get_color_eq_red hr h_rb_r, subst h_c₂,
id               └─────────────────┘ └┘ └────┘        └──┘
src      └──────┘└─────────────────┘          └────┘
typ      └──────┘└─────────────────┘└┘└────┘  └────┘└──┘
doc      └──────┘                             └────┘
txt      └──────┘                             └────┘
par      └──────┘                             └────┘
pid      └───┘└─┘                                  
st   ────────────────────────────────────────┘└──────────┘└─
717      simp [ins_rb_result] at ih,
id             └───────────┘
src      └────┘└───────────┘└─────┘
typ      └────┘└───────────┘└─────┘
doc      └────┘             └─────┘
txt      └────┘             └─────┘
par      └────┘             └─────┘
pid                       └───┘
st   ─────────────────────────────┘└─
718      apply balance2_node_rb; assumption },
id             └──────────────┘
src      └────┘└──────────────┘  └─────────┘
typ      └────┘└──────────────┘  └─────────┘
doc      └────┘                  └─────────┘
txt      └────┘                  └─────────┘
par      └────┘                  └─────────┘
pid                                       
st   ──────────────────────────────────────┘└┘
719    { specialize ih h_rb_r,
id                  └┘ └────┘
src      └─────────┘  
typ      └─────────┘└┘└────┘
doc      └─────────┘  
txt      └─────────┘  
par      └─────────┘  
pid                  
st   ───────────────────────┘└─
720      have := of_get_color_ne_red hnr h_rb_r, subst h_c₂,
id               └─────────────────┘ └─┘ └────┘        └──┘
src      └──────┘└─────────────────┘           └────┘
typ      └──────┘└─────────────────┘└─┘└────┘  └────┘└──┘
doc      └──────┘                              └────┘
txt      └──────┘                              └────┘
par      └──────┘                              └────┘
pid      └───┘└─┘                                   
st   ─────────────────────────────────────────┘└──────────┘└─
721      simp [ins_rb_result] at ih, cases ih,
id             └───────────┘               └┘
src      └────┘└───────────┘└─────┘  └────┘
typ      └────┘└───────────┘└─────┘  └────┘└┘
doc      └────┘             └─────┘  └────┘
txt      └────┘             └─────┘  └────┘
par      └────┘             └─────┘  └────┘
pid                       └───┘       
st   ─────────────────────────────┘└────────┘└─
722      constructor, constructor; assumption }
src      └─────────┘  └─────────┘  └─────────┘
typ      └─────────┘  └─────────┘  └─────────┘
doc      └─────────┘  └─────────┘  └─────────┘
txt      └─────────┘  └─────────┘  └─────────┘
par      └─────────┘  └─────────┘  └─────────┘
pid                                          
st   ──────────────┘└────────────────────────┘└─
723  end
st   ──┘
724  
725  def insert_rb_result : rbnode α → color → nat → Prop
id                          └────┘   └───┘   └─┘
src                         └────┘     └───┘   └─┘
typ                         └────┘   └───┘   └─┘
726  | t red n   := is_red_black t black (succ n)
id      └─┘       └──────────┘   └───┘  └──┘
src      └─┘        └──────────┘   └───┘  └──┘
typ     └─┘       └──────────┘   └───┘  └──┘
727  | t black n := ∃ c, is_red_black t c n
id      └───┘       └──────────┘   
src      └───┘         └──────────┘
typ     └───┘       └──────────┘   
728  
729  lemma insert_rb {t : rbnode α} (x) {c n} (h : is_red_black t c n) : insert_rb_result (insert lt t x) c n :=
id                        └────┘                  └──────────┘       └──────────────┘  └────┘ └┘     
src                       └────┘                   └──────────┘          └──────────────┘  └────┘
typ                       └────┘                  └──────────┘       └──────────────┘  └────┘ └┘     
730  begin
st   └─────
731    simp [insert],
id           └────┘
src    └────┘└────┘
typ    └────┘└────┘
doc    └────┘      
txt    └────┘      
par    └────┘      
pid              
st   ──────────────┘└─
732    have hi := ins_rb lt x h,
id                └────┘ └┘  
src    └─────────┘└────┘   
typ    └─────────┘└────┘└┘
doc    └─────────┘         
txt    └─────────┘         
par    └─────────┘         
pid    └─────┘└─┘         
st   ─────────────────────────┘└─
733    generalize he : ins lt t x = r,
id                     └─┘ └┘  
src    └──────────────┘└─┘     
typ    └──────────────┘└─┘└┘ 
doc    └──────────────┘        
txt    └──────────────┘        
par    └──────────────┘        
pid              └─┘└┘        
st   ───────────────────────────────┘└─
734    simp [he] at hi,
id           └┘
src    └────┘  └─────┘
typ    └────┘└┘└─────┘
doc    └────┘  └─────┘
txt    └────┘  └─────┘
par    └────┘  └─────┘
pid          └───┘
st   ────────────────┘└─
735    cases h; simp [get_color, ins_rb_result, insert_rb_result, mk_insert_result] at *,
id                   └───────┘  └───────────┘  └──────────────┘  └──────────────┘
src    └────┘   └────┘└───────┘└┘└───────────┘└┘└──────────────┘└┘└──────────────┘└────┘
typ    └────┘  └────┘└───────┘└┘└───────────┘└┘└──────────────┘└┘└──────────────┘└────┘
doc    └────┘   └────┘         └┘             └┘                └┘                └────┘
txt    └────┘   └────┘         └┘             └┘                └┘                └────┘
par    └────┘   └────┘         └┘             └┘                └┘                └────┘
pid                         └┘             └┘                └┘                └──┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
736    assumption',
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
st   ────────────┘└─
737    { cases hi, simp [mk_insert_result], constructor; assumption }
id             └┘        └──────────────┘
src      └────┘    └────┘└──────────────┘  └─────────┘  └─────────┘
typ      └────┘└┘  └────┘└──────────────┘  └─────────┘  └─────────┘
doc      └────┘    └────┘                  └─────────┘  └─────────┘
txt      └────┘    └────┘                  └─────────┘  └─────────┘
par      └────┘    └────┘                  └─────────┘  └─────────┘
pid                                                            
st   ───────────┘└───────────────────────┘└────────────────────────┘└─
738  end
st   ──┘
739  
740  lemma insert_is_red_black {t : rbnode α} {c n} (x) : is_red_black t c n → ∃ c n, is_red_black (insert lt t x) c n :=
id                                  └────┘               └──────────┘         └──────────┘  └────┘ └┘     
src                                 └────┘                └──────────┘              └──────────┘  └────┘
typ                                 └────┘               └──────────┘         └──────────┘  └────┘ └┘     
741  begin
st   └─────
742    intro h,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
743    have := insert_rb lt x h,
id             └───────┘ └┘  
src    └──────┘└───────┘   
typ    └──────┘└───────┘└┘
doc    └──────┘            
txt    └──────┘            
par    └──────┘            
pid    └───┘└─┘            
st   ─────────────────────────┘└─
744    cases c; simp [insert_rb_result] at this,
id                   └──────────────┘
src    └────┘   └────┘└──────────────┘└───────┘
typ    └────┘  └────┘└──────────────┘└───────┘
doc    └────┘   └────┘                └───────┘
txt    └────┘   └────┘                └───────┘
par    └────┘   └────┘                └───────┘
pid                                └─────┘
st   ─────────────────────────────────────────┘└─
745    { constructor, constructor, assumption },
src      └─────────┘  └─────────┘  └─────────┘
typ      └─────────┘  └─────────┘  └─────────┘
doc      └─────────┘  └─────────┘  └─────────┘
txt      └─────────┘  └─────────┘  └─────────┘
par      └─────────┘  └─────────┘  └─────────┘
pid                                          
st   ───┘└─────────┘└───────────┘└───────────┘└┘
746    { cases this, constructor, constructor, assumption }
id             └──┘
src      └────┘      └─────────┘  └─────────┘  └─────────┘
typ      └────┘└──┘  └─────────┘  └─────────┘  └─────────┘
doc      └────┘      └─────────┘  └─────────┘  └─────────┘
txt      └────┘      └─────────┘  └─────────┘  └─────────┘
par      └────┘      └─────────┘  └─────────┘  └─────────┘
pid                                                     
st   ─────────────┘└───────────┘└───────────┘└───────────┘└─
747  end
st   ──┘
748  
749  end is_red_black
750  
751  end rbnode